Library prosa.analysis.facts.model.task_arrivals


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


Require Export prosa.model.task.arrivals.
Require Export prosa.util.all.
Require Export prosa.analysis.facts.behavior.arrivals.

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.
We show that the number of arrivals of task can be split into disjoint intervals.
  Lemma num_arrivals_of_task_cat:
     tsk t t1 t2,
      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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 352)
  
  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

----------------------------------------------------------------------------- *)


  Proof.
    movetsk t t1 t2 /andP [GE LE].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 396)
  
  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

----------------------------------------------------------------------------- *)


    rewrite /number_of_task_arrivals /task_arrivals_between /arrivals_between.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 413)
  
  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<=t0<t2|true)arrivals_at arr_seq t0
       | job_task j == tsk] =
  size
    [seq j <- \cat_(t1<=t0<t|true)arrivals_at arr_seq t0 | job_task j == tsk] +
  size
    [seq j <- \cat_(t<=t0<t2|true)arrivals_at arr_seq t0 | job_task j == tsk]

----------------------------------------------------------------------------- *)


    now rewrite (@big_cat_nat _ _ _ t) //= filter_cat size_cat.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

To simplify subsequent proofs, we further lift [arrivals_between_cat] to the filtered version [task_arrivals_between].
  Lemma task_arrivals_between_cat:
     tsk t1 t t2,
      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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 372)
  
  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

----------------------------------------------------------------------------- *)


  Proof.
    movetsk t1 t t2 LEQ_t1 LEQ_t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 378)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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].
  Lemma task_arrivals_up_to_prefix_cat:
     j1 j2,
      arrives_in arr_seq j1
      arrives_in arr_seq j2
      job_task j1 = job_task j2
      job_arrival j1 job_arrival j2
      prefix Job (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 397)
  
  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 Job (task_arrivals_up_to_job_arrival arr_seq j1)
    (task_arrivals_up_to_job_arrival arr_seq j2)

----------------------------------------------------------------------------- *)


  Proof.
    intros j1 j2 ARR1 ARR2 TSK ARR_LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 403)
  
  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 Job (task_arrivals_up_to_job_arrival arr_seq j1)
    (task_arrivals_up_to_job_arrival arr_seq j2)

----------------------------------------------------------------------------- *)


     (task_arrivals_between arr_seq (job_task j1) (job_arrival j1 + 1) (job_arrival j2 + 1)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 415)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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].
  Lemma arrives_in_task_arrivals_up_to:
     j,
      arrives_in arr_seq j
      j \in task_arrivals_up_to_job_arrival arr_seq j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 408)
  
  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

----------------------------------------------------------------------------- *)


  Proof.
    intros j ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 410)
  
  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

----------------------------------------------------------------------------- *)


    rewrite mem_filter; apply /andP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 440)
  
  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_task j == job_task j /\
  j \in arrivals_between arr_seq 0 (succn (job_arrival j))

----------------------------------------------------------------------------- *)


    split; first by apply /eqP ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 443)
  
  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 (succn (job_arrival j))

----------------------------------------------------------------------------- *)


    move : ARR ⇒ [t ARR]; move : (ARR) ⇒ EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 486)
  
  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 (succn (job_arrival j))

----------------------------------------------------------------------------- *)


    apply H_consistent_arrivals in EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 487)
  
  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 (succn (job_arrival j))

----------------------------------------------------------------------------- *)


    rewrite (mem_bigcat_nat _ (fun tarrivals_at arr_seq t) j 0 _ (job_arrival j)) // EQ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 534)
  
  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 < succn t

----------------------------------------------------------------------------- *)


    now ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

Also, any job [j] from the arrival sequence is contained in [task_arrivals_at_job_arrival j].
  Lemma arrives_in_task_arrivals_at:
     j,
      arrives_in arr_seq j
      j \in task_arrivals_at_job_arrival arr_seq j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 419)
  
  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

----------------------------------------------------------------------------- *)


  Proof.
    intros j ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 421)
  
  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

----------------------------------------------------------------------------- *)


    rewrite mem_filter; apply /andP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 451)
  
  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_task j == job_task j /\ j \in arrivals_at arr_seq (job_arrival j)

----------------------------------------------------------------------------- *)


    split; first by apply /eqP ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 454)
  
  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)

----------------------------------------------------------------------------- *)


    rewrite /arrivals_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 485)
  
  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)

----------------------------------------------------------------------------- *)


    move : ARR ⇒ [t ARR].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 498)
  
  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).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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].
  Lemma task_arrivals_cat:
     t_m t,
      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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 434)
  
  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 (succn t_m) (succn t)

----------------------------------------------------------------------------- *)


  Proof.
    intros t1 t2 INEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 437)
  
  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 (succn t1) (succn t2)

----------------------------------------------------------------------------- *)


    now rewrite -filter_cat -arrivals_between_cat.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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].
  Lemma task_arrivals_up_to_cat:
     j,
      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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 452)
  
  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

----------------------------------------------------------------------------- *)


  Proof.
    intros j ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 454)
  
  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

----------------------------------------------------------------------------- *)


    rewrite /task_arrivals_up_to_job_arrival /task_arrivals_up_to
            /task_arrivals_before /task_arrivals_between.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 484)
  
  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 (succn (job_arrival j))
     | job_task j0 == job_task j] =
  task_arrivals_before_job_arrival arr_seq j ++
  task_arrivals_at_job_arrival arr_seq j

----------------------------------------------------------------------------- *)


    rewrite -filter_cat (arrivals_between_cat _ 0 (job_arrival j) (job_arrival j).+1) //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 508)
  
  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) (succn (job_arrival j))
     | job_task j0 == job_task j] =
  [seq j0 <- arrivals_between arr_seq 0 (job_arrival j) ++
             arrivals_at arr_seq (job_arrival j)
     | job_task j0 == job_task j]

----------------------------------------------------------------------------- *)


    now rewrite /arrivals_between big_nat1.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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).
  Lemma job_in_task_arrivals_between:
     j t1 t2,
      arrives_in arr_seq j
      job_task j = tsk
      t1 job_arrival j < t2
      j \in task_arrivals_between arr_seq tsk t1 t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 473)
  
  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

----------------------------------------------------------------------------- *)


  Proof.
    intros × ARR TSK INEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 479)
  
  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

----------------------------------------------------------------------------- *)


    rewrite mem_filter; apply/andP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 509)
  
  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_task j == tsk /\ j \in arrivals_between arr_seq t1 t2

----------------------------------------------------------------------------- *)


    split; first by apply /eqP ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 512)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

Any job [j] in [task_arrivals_between arr_seq tsk t1 t2] arrives in the arrival sequence [arr_seq].
  Lemma arrives_in_task_arrivals_implies_arrived:
     t1 t2 j,
      j \in (task_arrivals_between arr_seq tsk t1 t2)
      arrives_in arr_seq j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 486)
  
  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

----------------------------------------------------------------------------- *)


  Proof.
    intros × JB_IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 490)
  
  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
  JB_IN : j \in task_arrivals_between arr_seq tsk t1 t2
  ============================
  arrives_in arr_seq j

----------------------------------------------------------------------------- *)


    move : JB_IN; rewrite mem_filter; move ⇒ /andP [/eqP TSK JB_IN].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 570)
  
  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
  TSK : job_task j = tsk
  JB_IN : j \in arrivals_between arr_seq t1 t2
  ============================
  arrives_in arr_seq j

----------------------------------------------------------------------------- *)


    now apply in_arrivals_implies_arrived in JB_IN.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

An arrival sequence with non-duplicate arrivals implies that the task arrivals also contain non-duplicate arrivals.
  Lemma uniq_task_arrivals:
     t,
      arrival_sequence_uniq arr_seq
      uniq (task_arrivals_up_to arr_seq tsk t).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 493)
  
  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)

----------------------------------------------------------------------------- *)


  Proof.
    intros × UNQ_SEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 495)
  
  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)

----------------------------------------------------------------------------- *)


    apply filter_uniq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 496)
  
  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 (succn t))

----------------------------------------------------------------------------- *)


    now apply arrivals_uniq.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

A job cannot arrive before it's arrival time.
  Lemma job_notin_task_arrivals_before:
     j t,
      arrives_in arr_seq j
      job_arrival j > t
      j \notin task_arrivals_up_to arr_seq (job_task j) t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 509)
  
  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

----------------------------------------------------------------------------- *)


  Proof.
    intros j t ARR INEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 513)
  
  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

----------------------------------------------------------------------------- *)


    apply /negP; rewrite mem_filter ⇒ /andP [_ IN].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 580)
  
  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 (succn t)
  ============================
  False

----------------------------------------------------------------------------- *)


    apply mem_bigcat_nat_exists in IN; move : IN ⇒ [t' [IN NEQt']].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 605)
  
  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' < succn t
  ============================
  False

----------------------------------------------------------------------------- *)


    rewrite -(H_consistent_arrivals j t') in NEQt' ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 630)
  
  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 < succn t
  ============================
  False

----------------------------------------------------------------------------- *)


    now ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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].
  Lemma arrival_lt_implies_strict_prefix:
     j1 j2,
      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 _ (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 540)
  
  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 Job (task_arrivals_up_to_job_arrival arr_seq j1)
    (task_arrivals_up_to_job_arrival arr_seq j2)

----------------------------------------------------------------------------- *)


  Proof.
    intros j1 j2 TSK1 TSK2 ARR_1 ARR_2 ARR_INEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 547)
  
  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 Job (task_arrivals_up_to_job_arrival arr_seq j1)
    (task_arrivals_up_to_job_arrival arr_seq j2)

----------------------------------------------------------------------------- *)


     (task_arrivals_between arr_seq tsk ((job_arrival j1).+1) ((job_arrival j2).+1)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 556)
  
  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 (succn (job_arrival j1))
    (succn (job_arrival j2)) <> [::] /\
  task_arrivals_up_to_job_arrival arr_seq j1 ++
  task_arrivals_between arr_seq tsk (succn (job_arrival j1))
    (succn (job_arrival j2)) = task_arrivals_up_to_job_arrival arr_seq j2

----------------------------------------------------------------------------- *)


    split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 558)
  
  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 (succn (job_arrival j1))
    (succn (job_arrival j2)) <> [::]

subgoal 2 (ID 559) is:
 task_arrivals_up_to_job_arrival arr_seq j1 ++
 task_arrivals_between arr_seq tsk (succn (job_arrival j1))
   (succn (job_arrival j2)) = task_arrivals_up_to_job_arrival arr_seq j2

----------------------------------------------------------------------------- *)


    - move: (in_nil j2) ⇒ /negPJIN NIL.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 603)
  
  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 (succn (job_arrival j1))
          (succn (job_arrival j2)) = [::]
  ============================
  False

subgoal 2 (ID 559) is:
 task_arrivals_up_to_job_arrival arr_seq j1 ++
 task_arrivals_between arr_seq tsk (succn (job_arrival j1))
   (succn (job_arrival j2)) = task_arrivals_up_to_job_arrival arr_seq j2

----------------------------------------------------------------------------- *)


      rewrite -NIL in JIN; contradict JIN.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 630)
  
  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 (succn (job_arrival j1))
          (succn (job_arrival j2)) = [::]
  ============================
  j2
    \in task_arrivals_between arr_seq tsk (succn (job_arrival j1))
          (succn (job_arrival j2))

subgoal 2 (ID 559) is:
 task_arrivals_up_to_job_arrival arr_seq j1 ++
 task_arrivals_between arr_seq tsk (succn (job_arrival j1))
   (succn (job_arrival j2)) = task_arrivals_up_to_job_arrival arr_seq j2

----------------------------------------------------------------------------- *)


      now apply job_in_task_arrivals_between ⇒ //; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 559)
  
  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 (succn (job_arrival j1))
    (succn (job_arrival j2)) = task_arrivals_up_to_job_arrival arr_seq j2

----------------------------------------------------------------------------- *)


    - rewrite /task_arrivals_up_to_job_arrival TSK1 TSK2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 913)
  
  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 (succn (job_arrival j1))
    (succn (job_arrival j2)) =
  task_arrivals_up_to arr_seq tsk (job_arrival j2)

----------------------------------------------------------------------------- *)


      now rewrite -task_arrivals_cat; try by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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.
  Lemma nth_job_of_task_arrivals:
     n j_def j t,
      arrives_in arr_seq j
      job_task j = tsk
      job_index arr_seq j = n
      t job_arrival j
      nth j_def (task_arrivals_up_to arr_seq tsk t) n = j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 566)
  
  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

----------------------------------------------------------------------------- *)


  Proof.
    intros × ARR TSK IND T_G.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 574)
  
  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

----------------------------------------------------------------------------- *)


    rewrite -IND.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 576)
  
  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

----------------------------------------------------------------------------- *)


    have EQ_IND : index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 588)
  
  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)

subgoal 2 (ID 590) is:
 nth j_def (task_arrivals_up_to arr_seq tsk t) (job_index arr_seq j) = j

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 588)
  
  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)

----------------------------------------------------------------------------- *)


have CAT : xs, task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 603)
  
  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

subgoal 2 (ID 605) is:
 index j (task_arrivals_up_to_job_arrival arr_seq j) =
 index j (task_arrivals_up_to arr_seq tsk t)

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 603)
  
  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

----------------------------------------------------------------------------- *)


rewrite /task_arrivals_up_to_job_arrival TSK.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 616)
  
  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

----------------------------------------------------------------------------- *)


         (task_arrivals_between arr_seq tsk ((job_arrival j).+1) t.+1).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 623)
  
  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 (succn (job_arrival j)) (succn t) =
  task_arrivals_up_to arr_seq tsk t

----------------------------------------------------------------------------- *)


        now rewrite -task_arrivals_cat.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 605)

subgoal 1 (ID 605) is:
 index j (task_arrivals_up_to_job_arrival arr_seq j) =
 index j (task_arrivals_up_to arr_seq tsk t)
subgoal 2 (ID 590) is:
 nth j_def (task_arrivals_up_to arr_seq tsk t) (job_index arr_seq j) = j

----------------------------------------------------------------------------- *)


      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 605)
  
  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)

----------------------------------------------------------------------------- *)


      move : CAT ⇒ [xs ARR_CAT].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 642)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 590)

subgoal 1 (ID 590) is:
 nth j_def (task_arrivals_up_to arr_seq tsk t) (job_index arr_seq j) = j

----------------------------------------------------------------------------- *)


    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 590)
  
  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

----------------------------------------------------------------------------- *)


    rewrite /job_index EQ_IND nth_index ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 678)
  
  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

----------------------------------------------------------------------------- *)


    rewrite mem_filter; apply /andP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 730)
  
  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_task j == tsk /\ j \in arrivals_between arr_seq 0 (succn t)

----------------------------------------------------------------------------- *)


    split; first by apply /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 733)
  
  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 (succn t)

----------------------------------------------------------------------------- *)


    now apply job_in_arrivals_between ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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).
  Lemma task_arrivals_between_is_cat_of_task_arrivals_at:
     t1 t2,
      task_arrivals_between arr_seq tsk t1 t2 = \cat_(t1 t < t2) task_arrivals_at arr_seq tsk t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 583)
  
  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|true)task_arrivals_at arr_seq tsk t

----------------------------------------------------------------------------- *)


  Proof.
    intros ×.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 585)
  
  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|true)task_arrivals_at arr_seq tsk t

----------------------------------------------------------------------------- *)


    rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 602)
  
  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|true)arrivals_at arr_seq t | job_task j == tsk] =
  \cat_(t1<=t<t2|true)[seq j <- arrivals_at arr_seq t | job_task j == tsk]

----------------------------------------------------------------------------- *)


    now apply cat_filter_eq_filter_cat.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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).
  Lemma size_of_task_arrivals_between:
     t1 t2,
      size (task_arrivals_between arr_seq tsk t1 t2)
      = \sum_(t1 t < t2) size (task_arrivals_at arr_seq tsk t).
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 600)
  
  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)

----------------------------------------------------------------------------- *)


  Proof.
    intros ×.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 602)
  
  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)

----------------------------------------------------------------------------- *)


    rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 619)
  
  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|true)arrivals_at arr_seq t | job_task j == tsk] =
  \sum_(t1 <= t < t2)
     size [seq j <- arrivals_at arr_seq t | job_task j == tsk]

----------------------------------------------------------------------------- *)


    now rewrite size_big_nat cat_filter_eq_filter_cat.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End TaskArrivals.