In this file, we establish basic facts about the workload of sets of jobs.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.
Context {Job : JobType}.
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.
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.
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.
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.
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.