# 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}.

To begin with, we establish an auxiliary rewriting lemma that allows us to introduce a filter on the considered set of jobs, provided the filter predicate P2 is implied by the job-selection predicate P1.
Next, consider any job arrival sequence consistent with the arrival times of the jobs.
If at some point in time t the predicate P by which we select jobs from the set of arrivals in an interval `[t1, t2)` becomes certainly false, then we may disregard all jobs arriving at time t or later.
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.
In this section, we prove a few useful properties regarding the predicate of workload_of_jobs.
Section PredicateProperties.

First, we show that workload of jobs for an unsatisfiable predicate is equal to 0.
Next, consider two arbitrary predicates P and P'.
Variable P P' : pred Job.

We show that workload_of_jobs conditioned on P can be split into two summands: (1) workload_of_jobs conditioned on P P' and (2) workload_of_jobs conditioned on P ~~ P'.
We show that if P is indistinguishable from P' on set jobs, then workload_of_jobs conditioned on P is equal to workload_of_jobs conditioned on P'.