workload.v

Require Export prosa.model.aggregate.workload.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]
Require Export prosa.analysis.facts.behavior.arrivals.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]

(** * Lemmas about Workload of Sets of Jobs *)
(** In this file, we establish basic facts about the workload of sets of jobs. *)  
Section WorkloadFacts.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

  (**  ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** Further, consider any job arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.
  
  (** For simplicity, let's define a local name. *)
  Let arrivals_between := arrivals_between arr_seq.
  
  (** We observe that the cumulative workload of all jobs arriving in a time
      interval <<[t1, t2)>> and respecting a predicate [P] can be split into two parts. *)
  Lemma workload_of_jobs_cat:
    forall t t1 t2 P,
      t1 <= t <= t2 ->
      workload_of_jobs P (arrivals_between t1 t2) =
      workload_of_jobs P (arrivals_between t1 t) + workload_of_jobs P (arrivals_between t t2).Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
forall (t t1 t2 : nat) (P : pred Job),
t1 <= t <= t2 ->
workload_of_jobs P (arrivals_between t1 t2) =
workload_of_jobs P (arrivals_between t1 t) +
workload_of_jobs P (arrivals_between t t2)
  Proof.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
forall (t t1 t2 : nat) (P : pred Job),
t1 <= t <= t2 ->
workload_of_jobs P (arrivals_between t1 t2) =
workload_of_jobs P (arrivals_between t1 t) +
workload_of_jobs P (arrivals_between t t2)
    move => t t1 t2 P /andP [GE LE].Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
t, t1, t2: nat
P: pred Job
GE: t1 <= t
LE: t <= t2
workload_of_jobs P (arrivals_between t1 t2) =
workload_of_jobs P (arrivals_between t1 t) +
workload_of_jobs P (arrivals_between t t2)
    rewrite /workload_of_jobs /arrivals_between.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
t, t1, t2: nat
P: pred Job
GE: t1 <= t
LE: t <= t2
\sum_(j <- arrival_sequence.arrivals_between arr_seq
             t1 t2 | P j) job_cost j =
\sum_(j <- arrival_sequence.arrivals_between arr_seq
             t1 t | P j) job_cost j +
\sum_(j <- arrival_sequence.arrivals_between arr_seq t
             t2 | P j) job_cost j
    by rewrite (arrivals_between_cat _ _ t) // big_cat.
  Qed.

  (** Consider a job [j] ... *)
  Variable j : Job.

  (** ... and a duplicate-free sequence of jobs [jobs]. *)
  Variable jobs : seq Job.
  Hypothesis H_jobs_uniq : uniq jobs.

  (** Further, assume that [j] is contained in [jobs]. *)
  Hypothesis H_j_in_jobs : j \in jobs.

  (** To help with rewriting, we prove that the workload of [jobs]
      minus the job cost of [j] is equal to the workload of all jobs
      except [j]. To define the workload of all jobs, since
      [workload_of_jobs] expects a predicate, we use [predT], which
      is the always-true predicate. *)
  Lemma workload_minus_job_cost :
    workload_of_jobs (fun jhp : Job => jhp != j) jobs =
    workload_of_jobs predT jobs - job_cost j.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
workload_of_jobs (fun jhp : Job => jhp != j) jobs =
workload_of_jobs predT jobs - job_cost j
  Proof.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
workload_of_jobs (fun jhp : Job => jhp != j) jobs =
workload_of_jobs predT jobs - job_cost j
    rewrite /workload_of_jobs (big_rem j) //=  eq_refl //= add0n.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
\sum_(y <- rem (T:=Job) j jobs | y != j) job_cost y =
\sum_(j <- jobs) job_cost j - job_cost j
    rewrite [in RHS](big_rem j) //= addnC -subnBA //= subnn subn0.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
\sum_(y <- rem (T:=Job) j jobs | y != j) job_cost y =
\sum_(y <- rem (T:=Job) j jobs) job_cost y
    rewrite [in LHS]big_seq_cond [in RHS]big_seq_cond.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
\sum_(i <- rem (T:=Job) j jobs | (i
                                    \in rem (T:=Job) j
                                          jobs) &&
                                 (i != j)) job_cost i =
\sum_(i <- rem (T:=Job) j jobs | (i
                                    \in rem (T:=Job) j
                                          jobs) &&
                                 true) job_cost i
    apply eq_bigl => j'.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
j': Job
(j' \in rem (T:=Job) j jobs) && (j' != j) =
(j' \in rem (T:=Job) j jobs) && true
    rewrite Bool.andb_true_r.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
j': Job
(j' \in rem (T:=Job) j jobs) && (j' != j) =
(j' \in rem (T:=Job) j jobs)
    destruct (j' \in rem (T:=Job) j jobs) eqn:INjobs; last by done.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
j': Job
INjobs: (j' \in rem (T:=Job) j jobs) = true
true && (j' != j) = true
    apply /negP => /eqP EQUAL.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
j': Job
INjobs: (j' \in rem (T:=Job) j jobs) = true
EQUAL: j' = j
False
    by rewrite EQUAL mem_rem_uniqF in INjobs.
  Qed.

  (** In this section, we prove the relation between two different ways of constraining 
      [workload_of_jobs] to only those jobs that arrive prior to a given time. *)
  Section Subset.

    (** Assume that arrival times are consistent and that arrivals are unique. *)
    Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
    Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.

    (** Consider a time interval <<[t1, t2)>> and a time instant [t]. *)
    Variable t1 t2 t : instant.
    Hypothesis H_t1_le_t2 : t1 <= t2.

    (** Let [P] be an arbitrary predicate on jobs. *)
    Variable P : pred Job.

    (** Consider the window <<[t1,t2)>>. We prove that the total workload of the jobs
        arriving in this window before some [t] is the same as the workload of the jobs
        arriving in <<[t1,t)>>. Note that we only require [t1] to be less-or-equal
        than [t2]. Consequently, the interval <<[t1,t)>> may be empty. *)
    Lemma workload_equal_subset :
      workload_of_jobs (fun j => (job_arrival j <= t) && P j) (arrivals_between t1 t2)
      <= workload_of_jobs (fun j => P j) (arrivals_between t1 (t + ε)).Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
H_t1_le_t2: t1 <= t2
P: pred Job
workload_of_jobs
  (fun j : Job => (job_arrival j <= t) && P j)
  (arrivals_between t1 t2) <=
workload_of_jobs [eta P] (arrivals_between t1 (t + ε))
    Proof.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
H_t1_le_t2: t1 <= t2
P: pred Job
workload_of_jobs
  (fun j : Job => (job_arrival j <= t) && P j)
  (arrivals_between t1 t2) <=
workload_of_jobs [eta P] (arrivals_between t1 (t + ε))
      clear H_jobs_uniq H_j_in_jobs H_t1_le_t2.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
workload_of_jobs
  (fun j : Job => (job_arrival j <= t) && P j)
  (arrivals_between t1 t2) <=
workload_of_jobs [eta P] (arrivals_between t1 (t + ε))
      rewrite /workload_of_jobs big_seq_cond.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
\sum_(i <- arrivals_between t1 t2 | [&& i
                                          \in arrivals_between
                                                t1 t2,
                                        job_arrival i <=
                                        t
                                      & P i])
   job_cost i <=
\sum_(j <- arrivals_between t1 (t + ε) | P j)
   job_cost j
      rewrite -[in X in X <= _]big_filter -[in X in _ <= X]big_filter.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
\sum_(i <- [seq i <- arrivals_between t1 t2
              | i \in arrivals_between t1 t2
              & (job_arrival i <= t) && P i])
   job_cost i <=
\sum_(i <- [seq x <- arrivals_between t1 (t + ε)
              | P x]) job_cost i
      apply leq_sum_sub_uniq; first by apply filter_uniq, arrivals_uniq.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
{subset [seq i <- arrivals_between t1 t2
           | i \in arrivals_between t1 t2
           & (job_arrival i <= t) && P i]
     <= [seq x <- arrivals_between t1 (t + ε) | P x]}
      move => j'; rewrite mem_filter => [/andP [/andP [A /andP [C D]] _]].Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'
j' \in [seq x <- arrivals_between t1 (t + ε) | P x]
      rewrite mem_filter; apply/andP; split; first by done.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'
j' \in arrivals_between t1 (t + ε)
      apply job_in_arrivals_between; eauto.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'
arrives_in arr_seq j'
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'
t1 <= job_arrival j' < t + ε
      -Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'
arrives_in arr_seq j'
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'
t1 <= job_arrival j' < t + ε by eapply in_arrivals_implies_arrived; eauto 2.Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'
t1 <= job_arrival j' < t + ε
      -Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'
t1 <= job_arrival j' < t + ε apply in_arrivals_implies_arrived_between in A; auto; move: A => /andP [A E].Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
t1, t2, t: instant
P: pred Job
j': Job
C: job_arrival j' <= t
D: P j'
A: t1 <= job_arrival j'
E: job_arrival j' < t2
t1 <= job_arrival j' < t + ε
        by unfold ε; apply/andP; split; lia.
    Qed.

  End Subset.

End WorkloadFacts.