Require Import prosa.model.priority.elf.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,coercions,default]
Notation "_ - _" was already used in scope
distn_scope. [notation-overridden,parsing,default]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.definitions.priority.classes.
Require Export prosa.analysis.facts.model.workload.

(** In this file, we prove lemmas that are useful when both an FP policy and
    a JLFP policy are present in context. *)

(** In this section, we prove a lemma about workload partitioning which is useful
    for reasoning about the interference bound function for the ELF scheduling policy. *)
Section WorkloadTaskSum.

  (** Consider any type of tasks with relative priority points...*)
  Context {Task : TaskType} `{PriorityPoint Task}.

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

  (** Let us consider an FP policy and a compatible JLFP policy present in context. *)
  Context {FP : FP_policy Task}.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP.

  (** Consider any valid arrival sequence [arr_seq]. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence (arr_seq).

  (** We consider an arbitrary task set [ts]... *)
  Variable ts : seq Task.
  Hypothesis H_task_set : uniq ts.

  (** ... and assume that all jobs stem from tasks in this task set. *)
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

  (** We define a predicate to identify others tasks which have equal priority as [tsk]. *)
  Definition other_ep_task := fun tsk_o => (ep_task tsk tsk_o) && (tsk_o != tsk).

  (** We consider a job [j] belonging to this task ... *)
  Variable j : Job.
  Hypothesis H_job_of_task : job_of_task tsk j.

  (** ... and focus on the jobs arriving in an arbitrary interval <<[t1, t2)>>. *)
  Variable t1 t2 : duration.

  (** We first consider jobs that belong to other tasks that have equal priority
      as [tsk] and have higher-or-equal priority [JLFP] than [j]. *)
  Definition hep_job_of_ep_other_task :=
    fun j' : Job =>
      hep_job j' j
      && ep_task (job_task j') (job_task j)
      && (job_task j' != job_task j).

  (** We then establish that the cumulative workload of these jobs can be partitioned
      task-wise. *)
  Lemma hep_workload_from_other_ep_partitioned_by_tasks :
    workload_of_jobs hep_job_of_ep_other_task (arrivals_between arr_seq t1 t2)
      = \sum_(tsk_o <- ts | other_ep_task tsk_o)
        workload_of_jobs
          (fun j0 => hep_job_of_ep_other_task j0 && (job_task j0 == tsk_o))
          (arrivals_between arr_seq t1 t2).
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
workload_of_jobs hep_job_of_ep_other_task
  (arrivals_between arr_seq t1 t2) =
\sum_(tsk_o <- ts | other_ep_task tsk_o)
   workload_of_jobs
     (fun j0 : Job =>
      hep_job_of_ep_other_task j0 &&
      (job_task j0 == tsk_o))
     (arrivals_between arr_seq t1 t2)
  Proof.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
workload_of_jobs hep_job_of_ep_other_task
  (arrivals_between arr_seq t1 t2) =
\sum_(tsk_o <- ts | other_ep_task tsk_o)
   workload_of_jobs
     (fun j0 : Job =>
      hep_job_of_ep_other_task j0 &&
      (job_task j0 == tsk_o))
     (arrivals_between arr_seq t1 t2)
    apply: workload_of_jobs_partitioned_by_tasks => //.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
{in arrivals_between arr_seq t1 t2,
  forall j : Job, job_task j \in ts}
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
{in arrivals_between arr_seq t1 t2,
  forall j : Job,
  hep_job_of_ep_other_task j ->
  other_ep_task (job_task j)}
    -
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
{in arrivals_between arr_seq t1 t2,
  forall j : Job, job_task j \in ts} by move=> j' IN'; apply/H_all_jobs_from_taskset/in_arrivals_implies_arrived/IN'.
    -
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
{in arrivals_between arr_seq t1 t2,
  forall j : Job,
  hep_job_of_ep_other_task j ->
  other_ep_task (job_task j)} move: H_job_of_task => /eqP TSK j' IN'.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
TSK: job_task j = tsk
j': Job
IN': j' \in arrivals_between arr_seq t1 t2
hep_job_of_ep_other_task j' ->
other_ep_task (job_task j')
      rewrite /other_ep_task /hep_job_of_ep_other_task TSK
        => /andP [/andP [_ EP] NEQ].
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
TSK: job_task j = tsk
j': Job
IN': j' \in arrivals_between arr_seq t1 t2
EP: ep_task (job_task j') tsk
NEQ: job_task j' != tsk
ep_task tsk (job_task j') && (job_task j' != tsk)
      apply/andP; split => //.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
TSK: job_task j = tsk
j': Job
IN': j' \in arrivals_between arr_seq t1 t2
EP: ep_task (job_task j') tsk
NEQ: job_task j' != tsk
ep_task tsk (job_task j')
      by rewrite ep_task_sym.
  Qed.

  (** Now we focus on jobs belonging to tasks which have higher priority than [tsk]. *)
  Definition from_hp_task (j' : Job) :=
    hp_task (job_task j') (job_task j).

  (** We also identify higher-or-equal-priority jobs [JLFP] that belong to
      (1) tasks having higher priority than [tsk] ... *)
  Definition hep_from_hp_task (j' : Job) :=
    hep_job j' j && hp_task (job_task j') (job_task j).

  (** ... (2) tasks having equal priority as [tsk]. *)
  Definition hep_from_ep_task (j' : Job) :=
    hep_job j' j && ep_task (job_task j') (job_task j).

  (** First, we establish that the cumulative workload of higher-or-equal-priority
      jobs belonging to tasks having higher priority than [tsk] is equal to the
      cumulative workload of jobs belonging to higher-priority tasks. *)
  Lemma hep_hp_workload_hp :
    workload_of_jobs hep_from_hp_task (arrivals_between arr_seq t1 t2)
    = workload_of_jobs from_hp_task (arrivals_between arr_seq t1 t2).
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
workload_of_jobs hep_from_hp_task
  (arrivals_between arr_seq t1 t2) =
workload_of_jobs from_hp_task
  (arrivals_between arr_seq t1 t2)
  Proof.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
workload_of_jobs hep_from_hp_task
  (arrivals_between arr_seq t1 t2) =
workload_of_jobs from_hp_task
  (arrivals_between arr_seq t1 t2)
    apply/eq_bigl =>j0; apply /idP/idP.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
hep_from_hp_task j0 -> from_hp_task j0
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
from_hp_task j0 -> hep_from_hp_task j0
    -
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
hep_from_hp_task j0 -> from_hp_task j0 by move=> /andP[].
    -
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
from_hp_task j0 -> hep_from_hp_task j0 move=> Hp; apply/andP; split =>//.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
Hp: from_hp_task j0
hep_job j0 j
      by apply: (hp_task_implies_hep_job JLFP FP).
  Qed.

  (** We then establish that the cumulative workload of higher-or-equal priority jobs
      is equal to the sum of cumulative workload of higher-or-equal priority jobs
      belonging to higher-priority tasks and the cumulative workload of
      higher-or-equal-priority jobs belonging to equal-priority tasks. *)
  Lemma hep_workload_partitioning_taskwise :
    workload_of_hep_jobs arr_seq j t1 t2
    = workload_of_jobs hep_from_hp_task (arrivals_between arr_seq t1 t2)
      + workload_of_jobs hep_from_ep_task (arrivals_between arr_seq t1 t2).
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
workload_of_hep_jobs arr_seq j t1 t2 =
workload_of_jobs hep_from_hp_task
  (arrivals_between arr_seq t1 t2) +
workload_of_jobs hep_from_ep_task
  (arrivals_between arr_seq t1 t2)
  Proof.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
workload_of_hep_jobs arr_seq j t1 t2 =
workload_of_jobs hep_from_hp_task
  (arrivals_between arr_seq t1 t2) +
workload_of_jobs hep_from_ep_task
  (arrivals_between arr_seq t1 t2)
    rewrite /workload_of_hep_jobs /workload_of_jobs.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
\sum_(j0 <- arrivals_between arr_seq t1 t2 | hep_job
                                               j0 j)
   job_cost j0 =
\sum_(j <- arrivals_between arr_seq t1 t2 | hep_from_hp_task
                                              j)
   job_cost j +
\sum_(j <- arrivals_between arr_seq t1 t2 | hep_from_ep_task
                                              j)
   job_cost j
    rewrite (bigID from_hp_task) /=; congr (_ + _); apply: eq_bigl => j0.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
hep_job j0 j && ~~ from_hp_task j0 =
hep_from_ep_task j0
    apply: andb_id2l => HEPj.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
~~ from_hp_task j0 =
ep_task (job_task j0) (job_task j)
    have HEPt : hep_task (job_task j0) (job_task j) by apply (hep_job_implies_hep_task JLFP).
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
HEPt: hep_task (job_task j0) (job_task j)
~~ from_hp_task j0 =
ep_task (job_task j0) (job_task j)
    apply/idP/idP; rewrite negb_and.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
HEPt: hep_task (job_task j0) (job_task j)
~~ hep_task (job_task j0) (job_task j)
|| ~~ ~~ hep_task (job_task j) (job_task j0) ->
ep_task (job_task j0) (job_task j)
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
HEPt: hep_task (job_task j0) (job_task j)
ep_task (job_task j0) (job_task j) ->
~~ hep_task (job_task j0) (job_task j)
|| ~~ ~~ hep_task (job_task j) (job_task j0)
    -
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
HEPt: hep_task (job_task j0) (job_task j)
~~ hep_task (job_task j0) (job_task j)
|| ~~ ~~ hep_task (job_task j) (job_task j0) ->
ep_task (job_task j0) (job_task j) move =>/orP[nHEPt| /negPn ?].
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
HEPt: hep_task (job_task j0) (job_task j)
nHEPt: ~~ hep_task (job_task j0) (job_task j)
ep_task (job_task j0) (job_task j)
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
HEPt: hep_task (job_task j0) (job_task j)
__view_subject_2_: hep_task (job_task j)
  (job_task j0)
ep_task (job_task j0) (job_task j)
      +
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
HEPt: hep_task (job_task j0) (job_task j)
nHEPt: ~~ hep_task (job_task j0) (job_task j)
ep_task (job_task j0) (job_task j) exfalso; by move: nHEPt; rewrite HEPt.
      +
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
HEPt: hep_task (job_task j0) (job_task j)
__view_subject_2_: hep_task (job_task j)
  (job_task j0)
ep_task (job_task j0) (job_task j) by apply/andP.
    -
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
H2: JobCost Job
FP: FP_policy Task
JLFP: JLFP_policy Job
JLFP_FP_is_compatible: JLFP_FP_compatible JLFP FP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: seq Task
H_task_set: uniq ts
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
j: Job
H_job_of_task: job_of_task tsk j
t1, t2: duration
j0: Job
HEPj: hep_job j0 j
HEPt: hep_task (job_task j0) (job_task j)
ep_task (job_task j0) (job_task j) ->
~~ hep_task (job_task j0) (job_task j)
|| ~~ ~~ hep_task (job_task j) (job_task j0) by move => /andP[? ?]; apply/orP; right; apply/negPn.
  Qed.

End WorkloadTaskSum.