Require Export prosa.analysis.facts.priority.classes.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_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]
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.definitions.interference.
Require Export prosa.analysis.definitions.priority.classes.
Require Export prosa.analysis.facts.model.service_of_jobs.

(** * Auxiliary Lemmas about Interference *)

(** If there is a priority policy in the context, one can
    differentiate between interference (interfering workload) that
    comes from jobs with higher or lower priority from other sources
    of interference (interfering workload).

    Unfortunately, instantiated functions usually do not come with any
    useful lemmas about them. In order to reuse existing lemmas, we
    need to prove equivalence of the instantiated functions to some
    conventional notions. *)

(** First, we prove several lemmas about interference in the context
    of priority policies involving both FP and JLFP relations. *)
Section InterferenceProperties.

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

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

  (** Consider any kind of processor state model. *)
  Context {PState : ProcessorState Job}.

  (** Consider any arrival sequence ... *)
  Variable arr_seq : arrival_sequence Job.

  (** ... and any schedule. *)
  Variable sched : schedule PState.

  (** Consider a reflexive FP-policy and a JLFP policy compatible with it. *)
  Context {FP : FP_policy Task} {JLFP : JLFP_policy Job}.
  Hypothesis H_compatible : JLFP_FP_compatible JLFP FP.
  Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.

  (** We observe that any higher-priority job must come from a task with
      either higher or equal priority. *)
  Lemma another_task_hep_job_split_hp_ep :
    forall j1 j2,
      another_task_hep_job j1 j2
      = hp_task_hep_job j1 j2 || other_ep_task_hep_job j1 j2.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
forall j1 j2 : Job,
another_task_hep_job j1 j2 =
hp_task_hep_job j1 j2 || other_ep_task_hep_job j1 j2
  Proof.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
forall j1 j2 : Job,
another_task_hep_job j1 j2 =
hp_task_hep_job j1 j2 || other_ep_task_hep_job j1 j2
    move=> j1 j2; rewrite -[X in _ || X]andbA -andb_orr /another_task_hep_job.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
j1, j2: Job
hep_job j1 j2 && (job_task j1 != job_task j2) =
hep_job j1 j2 &&
(hp_task (job_task j1) (job_task j2)
 || ep_task (job_task j1) (job_task j2) &&
    (job_task j1 != job_task j2))
    have [hepj1j2/=|//] := boolP (hep_job j1 j2).
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
j1, j2: Job
hepj1j2: hep_job j1 j2
(job_task j1 != job_task j2) =
hp_task (job_task j1) (job_task j2)
|| ep_task (job_task j1) (job_task j2) &&
   (job_task j1 != job_task j2)
    rewrite -[hp_task _ _](@andb_idr _ (job_task j1 != job_task j2)).
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
j1, j2: Job
hepj1j2: hep_job j1 j2
(job_task j1 != job_task j2) =
hp_task (job_task j1) (job_task j2) &&
(job_task j1 != job_task j2)
|| ep_task (job_task j1) (job_task j2) &&
   (job_task j1 != job_task j2)
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
j1, j2: Job
hepj1j2: hep_job j1 j2
hp_task (job_task j1) (job_task j2) ->
job_task j1 != job_task j2
    -
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
j1, j2: Job
hepj1j2: hep_job j1 j2
(job_task j1 != job_task j2) =
hp_task (job_task j1) (job_task j2) &&
(job_task j1 != job_task j2)
|| ep_task (job_task j1) (job_task j2) &&
   (job_task j1 != job_task j2) by rewrite -andb_orl -hep_hp_ep_task hep_job_implies_hep_task.
    -
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
j1, j2: Job
hepj1j2: hep_job j1 j2
hp_task (job_task j1) (job_task j2) ->
job_task j1 != job_task j2 by apply: contraTN => /eqP->; rewrite hp_task_irrefl.
  Qed.

  (** We establish a higher-or-equal job of another task causing interference,
      can be due to a higher priority task or an equal priority task. *)
  Lemma hep_interference_another_task_split :
    forall j t,
      another_task_hep_job_interference arr_seq sched j t
      = hep_job_from_hp_task_interference arr_seq sched j t
        || hep_job_from_other_ep_task_interference arr_seq sched j t.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
forall (j : Job) (t : instant),
another_task_hep_job_interference arr_seq sched j t =
hep_job_from_hp_task_interference arr_seq sched j t
|| hep_job_from_other_ep_task_interference arr_seq
     sched j t
  Proof.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
forall (j : Job) (t : instant),
another_task_hep_job_interference arr_seq sched j t =
hep_job_from_hp_task_interference arr_seq sched j t
|| hep_job_from_other_ep_task_interference arr_seq
     sched j t
    move => j t; rewrite -has_predU; apply: eq_in_has => j' _ /=.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
j: Job
t: instant
j': Job
another_task_hep_job j' j =
hp_task_hep_job j' j || other_ep_task_hep_job j' j
    exact: another_task_hep_job_split_hp_ep.
  Qed.

  (** Now, assuming a uniprocessor model,... *)
  Hypothesis H_uniproc : uniprocessor_model PState.

  (** ...the previous lemma allows us to establish that the cumulative interference incurred by a job
      is equal to the sum of the cumulative interference from higher-or-equal-priority jobs belonging to
      strictly higher-priority tasks (FP) and the cumulative interference from higher-or-equal-priority
      jobs belonging to equal-priority tasks (GEL). *)
  Lemma cumulative_hep_interference_split_tasks_new :
    forall j t1 Δ,
    cumulative_another_task_hep_job_interference arr_seq  sched j t1 (t1 + Δ)
    = cumulative_interference_from_hep_jobs_from_hp_tasks arr_seq sched j t1 (t1 + Δ)
      + cumulative_interference_from_hep_jobs_from_other_ep_tasks arr_seq sched j t1 (t1 + Δ).
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
forall (j : Job) (t1 : instant) (Δ : nat),
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 (t1 + Δ) =
cumulative_interference_from_hep_jobs_from_hp_tasks
  arr_seq sched j t1 (t1 + Δ) +
cumulative_interference_from_hep_jobs_from_other_ep_tasks
  arr_seq sched j t1 (t1 + Δ)
  Proof.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
forall (j : Job) (t1 : instant) (Δ : nat),
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 (t1 + Δ) =
cumulative_interference_from_hep_jobs_from_hp_tasks
  arr_seq sched j t1 (t1 + Δ) +
cumulative_interference_from_hep_jobs_from_other_ep_tasks
  arr_seq sched j t1 (t1 + Δ)
    move => j t1 Δ.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
j: Job
t1: instant
Δ: nat
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 (t1 + Δ) =
cumulative_interference_from_hep_jobs_from_hp_tasks
  arr_seq sched j t1 (t1 + Δ) +
cumulative_interference_from_hep_jobs_from_other_ep_tasks
  arr_seq sched j t1 (t1 + Δ)
    rewrite -big_split //=; apply: eq_big_seq => t IN.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
j: Job
t1: instant
Δ: nat
t: Datatypes_nat__canonical__eqtype_Equality
IN: t \in index_iota t1 (t1 + Δ)
another_task_hep_job_interference arr_seq sched j t =
hep_job_from_hp_task_interference arr_seq sched j t +
hep_job_from_other_ep_task_interference arr_seq sched
  j t
    rewrite hep_interference_another_task_split.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
j: Job
t1: instant
Δ: nat
t: Datatypes_nat__canonical__eqtype_Equality
IN: t \in index_iota t1 (t1 + Δ)
hep_job_from_hp_task_interference arr_seq sched j t
|| hep_job_from_other_ep_task_interference arr_seq
     sched j t =
hep_job_from_hp_task_interference arr_seq sched j t +
hep_job_from_other_ep_task_interference arr_seq sched
  j t
    have: forall a b, ~~ (a && b) -> (a || b) = a + b :> nat by case; case.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
j: Job
t1: instant
Δ: nat
t: Datatypes_nat__canonical__eqtype_Equality
IN: t \in index_iota t1 (t1 + Δ)
(forall a b : bool, ~~ (a && b) -> a || b = a + b) ->
hep_job_from_hp_task_interference arr_seq sched j t
|| hep_job_from_other_ep_task_interference arr_seq
     sched j t =
hep_job_from_hp_task_interference arr_seq sched j t +
hep_job_from_other_ep_task_interference arr_seq sched
  j t
    apply; apply/negP => /andP[/hasP[j' + hp] /hasP[j'' + ep]].
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
j: Job
t1: instant
Δ: nat
t: Datatypes_nat__canonical__eqtype_Equality
IN: t \in index_iota t1 (t1 + Δ)
j': Job
hp: hp_task_hep_job j' j
j'': Job
ep: other_ep_task_hep_job j'' j
j' \in served_jobs_at arr_seq sched t ->
j'' \in served_jobs_at arr_seq sched t -> False
    rewrite !mem_filter => /andP[sj' _] /andP[sj'' _].
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
j: Job
t1: instant
Δ: nat
t: Datatypes_nat__canonical__eqtype_Equality
IN: t \in index_iota t1 (t1 + Δ)
j': Job
hp: hp_task_hep_job j' j
j'': Job
ep: other_ep_task_hep_job j'' j
sj': receives_service_at sched j' t
sj'': receives_service_at sched j'' t
False
    move: hp ep; have ->: j'' = j' by exact: only_one_job_receives_service_at_uni.
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
j: Job
t1: instant
Δ: nat
t: Datatypes_nat__canonical__eqtype_Equality
IN: t \in index_iota t1 (t1 + Δ)
j', j'': Job
sj': receives_service_at sched j' t
sj'': receives_service_at sched j'' t
hp_task_hep_job j' j ->
other_ep_task_hep_job j' j -> False
    move=> /andP[_ /andP[_ +]] /andP[/andP[_ +] _].
Task: TaskType
Job: JobType
jt: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FP: FP_policy Task
JLFP: JLFP_policy Job
H_compatible: JLFP_FP_compatible JLFP FP
H_reflexive_priorities: reflexive_task_priorities FP
H_uniproc: uniprocessor_model PState
j: Job
t1: instant
Δ: nat
t: Datatypes_nat__canonical__eqtype_Equality
IN: t \in index_iota t1 (t1 + Δ)
j', j'': Job
sj': receives_service_at sched j' t
sj'': receives_service_at sched j'' t
~~ hep_task (job_task j) (job_task j') ->
ep_task (job_task j') (job_task j) -> False
    by rewrite hep_hp_ep_task negb_or ep_task_sym => /andP[_ /negbTE].
  Qed.

End InterferenceProperties.

(** In the following section, we prove a few properties of
    interference under a JLFP policy. *)
Section InterferencePropertiesJLFP.

  (** 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}.

  (** Consider any kind of fully supply-consuming uniprocessor model. *)
  Context `{PState : ProcessorState Job}.
  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.

  (** Consider any valid arrival sequence with consistent arrivals ... *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** ... and any uni-processor schedule of this arrival
      sequence ... *)
  Variable sched : schedule PState.
  Hypothesis H_jobs_come_from_arrival_sequence :
    jobs_come_from_arrival_sequence sched arr_seq.

  (** ... where jobs do not execute before their arrival or after
      completion. *)
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

  (** Let [tsk] be any task. *)
  Variable tsk : Task.

  (** In the following, consider a JLFP-policy that indicates a
      higher-or-equal priority relation, and assume that this relation
      is reflexive and transitive. *)
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.

  (** First, we prove a few rewriting rules under the assumption that
      there is no supply. *)
  Section NoSupply.

    (** Consider a time instant [t] ... *)
    Variable t : instant.

    (** ... and assume that there is no supply at [t]. *)
    Hypothesis H_no_supply : ~~ has_supply sched t.

    (** Then, there is no interference from higher-or-equal priority
        jobs ... *)
    Lemma no_hep_job_interference_without_supply :
      forall j, ~~ another_hep_job_interference arr_seq sched j t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
forall j : Job,
~~ another_hep_job_interference arr_seq sched j t
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
forall j : Job,
~~ another_hep_job_interference arr_seq sched j t
      move=> j; apply/hasPn => [s IN]; exfalso.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
j, s: Job
IN: s \in served_jobs_at arr_seq sched t
False
      move: IN; rewrite mem_filter => /andP [SERV _].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
j, s: Job
SERV: receives_service_at sched s t
False
      move: (H_no_supply) => /negP NSUP; apply: NSUP.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
j, s: Job
SERV: receives_service_at sched s t
has_supply sched t
      by apply: receives_service_implies_has_supply.
    Qed.

    (** ... and that there is no interference from higher-or-equal
        priority jobs from other tasks. *)
    Lemma no_hep_task_interference_without_supply :
      forall j, ~~ another_task_hep_job_interference arr_seq sched j t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
forall j : Job,
~~ another_task_hep_job_interference arr_seq sched j t
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
forall j : Job,
~~ another_task_hep_job_interference arr_seq sched j t
      move=> j; apply/hasPn => [s IN]; exfalso.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
j, s: Job
IN: s \in served_jobs_at arr_seq sched t
False
      move: IN; rewrite mem_filter => /andP [SERV _].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
j, s: Job
SERV: receives_service_at sched s t
False
      move: (H_no_supply) => /negP NSUP; apply: NSUP.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_no_supply: ~~ has_supply sched t
j, s: Job
SERV: receives_service_at sched s t
has_supply sched t
      by apply: receives_service_implies_has_supply.
    Qed.

  End NoSupply.

  (** In the following subsection, we prove properties of the
      introduced functions under the assumption that the schedule is
      idle. *)
  Section Idle.

    (** Consider a time instant [t] ... *)
    Variable t : instant.

    (** ... and assume that the schedule is idle at [t]. *)
    Hypothesis H_idle : is_idle arr_seq sched t.

    (** We prove that in this case: ... *)

    (** ... there is no interference from higher-or-equal priority
        jobs ... *)
    Lemma no_hep_job_interference_when_idle :
      forall j, ~~ another_hep_job_interference arr_seq sched j t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_idle: is_idle arr_seq sched t
forall j : Job,
~~ another_hep_job_interference arr_seq sched j t
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_idle: is_idle arr_seq sched t
forall j : Job,
~~ another_hep_job_interference arr_seq sched j t
      move=> j; apply/hasPn=> jo SERV; exfalso.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_idle: is_idle arr_seq sched t
j, jo: Job
SERV: jo \in served_jobs_at arr_seq sched t
False
      rewrite mem_filter in SERV; move: SERV => /andP [SERV _].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_idle: is_idle arr_seq sched t
j, jo: Job
SERV: receives_service_at sched jo t
False
      by apply/negP; first apply: no_service_received_when_idle => //. 
    Qed.

    (** ... and that there is no interference from higher-or-equal
        priority jobs from other tasks. *)
    Lemma no_hep_task_interference_when_idle :
      forall j, ~~ another_task_hep_job_interference arr_seq sched j t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_idle: is_idle arr_seq sched t
forall j : Job,
~~ another_task_hep_job_interference arr_seq sched j t
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_idle: is_idle arr_seq sched t
forall j : Job,
~~ another_task_hep_job_interference arr_seq sched j t
      move=> j; apply/hasPn=> jo SERV; exfalso.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_idle: is_idle arr_seq sched t
j, jo: Job
SERV: jo \in served_jobs_at arr_seq sched t
False
      rewrite mem_filter in SERV; move: SERV => /andP [SERV _].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
t: instant
H_idle: is_idle arr_seq sched t
j, jo: Job
SERV: receives_service_at sched jo t
False
      by apply/negP; first apply: no_service_received_when_idle => //. 
    Qed.

  End Idle.

  (** Next, we prove properties of the introduced functions under the
      assumption that there is supply and the scheduler is not
      idle. *)
  Section SupplyAndScheduledJob.

    (** Consider a job [j] of task [tsk]. In this subsection, job [j]
        is deemed to be the main job with respect to which the
        functions are computed. *)
    Variable j : Job.
    Hypothesis H_j_tsk : job_of_task tsk j.

    (** Consider a time instant [t] ... *)
    Variable t : instant.

    (** ... and assume that there is supply at [t]. *)
    Hypothesis H_supply : has_supply sched t.

    (** First, consider a case when _some_ job is scheduled at time [t]. *)
    Section SomeJobIsScheduled.

      (** Consider a job [j'] (not necessarily distinct from job [j])
          that is scheduled at time [t]. *)
      Variable j' : Job.
      Hypothesis H_sched : scheduled_at sched j' t.

      (** Under the stated assumptions, we show that the interference
          from another higher-or-equal priority job is equivalent to
          the relation [another_hep_job]. *)
      Lemma interference_ahep_def :
        another_hep_job_interference arr_seq sched j t = another_hep_job j' j.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
another_hep_job_interference arr_seq sched j t =
another_hep_job j' j
      Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
another_hep_job_interference arr_seq sched j t =
another_hep_job j' j
        clear H_j_tsk.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
another_hep_job_interference arr_seq sched j t =
another_hep_job j' j
        apply/idP/idP => [/hasP[jhp /[!mem_filter]/andP[PSERV IN] AHEP] | AHEP].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
jhp: Job
PSERV: receives_service_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_hep_job jhp j
another_hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model
  PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_hep_job j' j
another_hep_job_interference arr_seq sched j t
        {
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
jhp: Job
PSERV: receives_service_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_hep_job jhp j
another_hep_job j' j apply service_at_implies_scheduled_at in PSERV.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
jhp: Job
PSERV: scheduled_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_hep_job jhp j
another_hep_job j' j
          have EQ: jhp = j' by apply: H_uniprocessor_proc_model.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
jhp: Job
PSERV: scheduled_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_hep_job jhp j
EQ: jhp = j'
another_hep_job j' j
          by subst j'. }
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_hep_job j' j
another_hep_job_interference arr_seq sched j t
        {
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_hep_job j' j
another_hep_job_interference arr_seq sched j t apply/hasP; exists j' => //.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_hep_job j' j
j' \in served_jobs_at arr_seq sched t
          by apply receives_service_and_served_at_consistent, ideal_progress_inside_supplies. }
      Qed.

      (** Similarly, we show that the interference from another
          higher-or-equal priority job from another task is equivalent
          to the relation [another_task_hep_job]. *)
      Lemma interference_athep_def :
        another_task_hep_job_interference arr_seq sched j t = another_task_hep_job j' j.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
another_task_hep_job_interference arr_seq sched j t =
another_task_hep_job j' j
      Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
another_task_hep_job_interference arr_seq sched j t =
another_task_hep_job j' j
        apply/idP/idP => [/hasP[jhp /[!mem_filter]/andP[PSERV IN] AHEP] | AHEP].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
jhp: Job
PSERV: receives_service_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_task_hep_job jhp j
another_task_hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model
  PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_task_hep_job j' j
another_task_hep_job_interference arr_seq sched j t
        -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
jhp: Job
PSERV: receives_service_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_task_hep_job jhp j
another_task_hep_job j' j apply service_at_implies_scheduled_at in PSERV.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
jhp: Job
PSERV: scheduled_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_task_hep_job jhp j
another_task_hep_job j' j
          have EQ: jhp = j' by apply: H_uniprocessor_proc_model.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
jhp: Job
PSERV: scheduled_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_task_hep_job jhp j
EQ: jhp = j'
another_task_hep_job j' j
          by subst.
        -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_task_hep_job j' j
another_task_hep_job_interference arr_seq sched j t apply/hasP; exists j' => //; rewrite mem_filter; apply/andP; split.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_task_hep_job j' j
receives_service_at sched j' t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model
  PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_task_hep_job j' j
j' \in arrivals_up_to arr_seq t
          +
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_task_hep_job j' j
receives_service_at sched j' t by apply: progress_inside_supplies => //.
          +
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_sched: scheduled_at sched j' t
AHEP: another_task_hep_job j' j
j' \in arrivals_up_to arr_seq t by apply: arrivals_up_to_scheduled_at.
      Qed.

    End SomeJobIsScheduled.

    (** Next, consider a case when [j] itself is scheduled at [t]. *)
    Section JIsScheduled.

      (** Assume that [j] is scheduled at time [t]. *)
      Hypothesis H_j_sched : scheduled_at sched j t.

      (** Then there is no interference from higher-or-equal priority
          jobs at time [t]. *)
      Lemma no_ahep_interference_when_scheduled :
        ~~ another_hep_job_interference arr_seq sched j t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_sched: scheduled_at sched j t
~~ another_hep_job_interference arr_seq sched j t
      Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_sched: scheduled_at sched j t
~~ another_hep_job_interference arr_seq sched j t
        apply/negP; move=> /hasP[jhp /[!mem_filter]/andP[PSERV IN] AHEP].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_sched: scheduled_at sched j t
jhp: Job
PSERV: receives_service_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_hep_job jhp j
False
        apply service_at_implies_scheduled_at in PSERV.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_sched: scheduled_at sched j t
jhp: Job
PSERV: scheduled_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_hep_job jhp j
False
        have EQ: jhp = j; [by apply: H_uniprocessor_proc_model | subst jhp].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_sched: scheduled_at sched j t
AHEP: another_hep_job j j
IN: j \in arrivals_up_to arr_seq t
PSERV: scheduled_at sched j t
False
        by apply another_hep_job_antireflexive in AHEP.
      Qed.

    End JIsScheduled.

    (** Next, consider a case when [j] receives service at [t]. *)
    Section JIsServed.

      (** Assume that [j] receives service at time [t]. *)
      Hypothesis H_j_served : receives_service_at sched j t.

      (** Then there is no interference from higher-or-equal priority
          jobs at time [t]. *)
      Lemma no_ahep_interference_when_served :
        ~~ another_hep_job_interference arr_seq sched j t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_served: receives_service_at sched j t
~~ another_hep_job_interference arr_seq sched j t
      Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_served: receives_service_at sched j t
~~ another_hep_job_interference arr_seq sched j t
        apply/negP => INT.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_served: receives_service_at sched j t
INT: another_hep_job_interference arr_seq sched j t
False
        rewrite (interference_ahep_def j) in INT => //; first last.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_served: receives_service_at sched j t
scheduled_at sched j t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model
  PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_served: receives_service_at sched j t
INT: another_hep_job j j
False
        -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_served: receives_service_at sched j t
scheduled_at sched j t by apply service_at_implies_scheduled_at.
        -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
H_j_served: receives_service_at sched j t
INT: another_hep_job j j
False by move: INT => /andP [_ ]; rewrite eq_refl.
      Qed.

    End JIsServed.

    (** In the next subsection, we consider a case when a job [j']
        from the same task (as job [j]) is scheduled. *)
    Section FromSameTask.

      (** Consider a job [j'] that comes from task [tsk] and is
          scheduled at time instant [t].  *)
      Variable j' : Job.
      Hypothesis H_j'_tsk : job_of_task tsk j'.
      Hypothesis H_j'_sched : scheduled_at sched j' t.

      (** Then we show that there is no interference from
          higher-or-equal priority jobs of another task. *)
      Lemma no_athep_interference_when_scheduled :
        ~~ another_task_hep_job_interference arr_seq sched j t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_tsk: job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
~~ another_task_hep_job_interference arr_seq sched j t
      Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_tsk: job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
~~ another_task_hep_job_interference arr_seq sched j t
        apply/negP; move=> /hasP[jhp /[!mem_filter]/andP[PSERV IN] AHEP].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_tsk: job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
jhp: Job
PSERV: receives_service_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_task_hep_job jhp j
False
        apply service_at_implies_scheduled_at in PSERV.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_tsk: job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
jhp: Job
PSERV: scheduled_at sched jhp t
IN: jhp \in arrivals_up_to arr_seq t
AHEP: another_task_hep_job jhp j
False
        have EQ: jhp = j'; [by apply: H_uniprocessor_proc_model | subst jhp].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_tsk: job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
AHEP: another_task_hep_job j' j
IN: j' \in arrivals_up_to arr_seq t
PSERV: scheduled_at sched j' t
False
        by eapply another_task_hep_job_taskwise_antireflexive in AHEP.
      Qed.

    End FromSameTask.

    (** In the next subsection, we consider a case when a job [j']
        from a task other than [j]'s task is scheduled. *)
    Section FromDifferentTask.

      (** Consider a job [j'] that _does_ _not_ comes from task
            [tsk] and is scheduled at time instant [t].  *)
      Variable j' : Job.
      Hypothesis H_j'_not_tsk : ~~ job_of_task tsk j'.
      Hypothesis H_j'_sched : scheduled_at sched j' t.

      (** We prove that then [j] incurs higher-or-equal priority
          interference from another task iff [j'] has higher-or-equal
          priority than [j]. *)
      Lemma athep_interference_iff :
        another_task_hep_job_interference arr_seq sched j t = hep_job j' j.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
another_task_hep_job_interference arr_seq sched j t =
hep_job j' j
      Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
another_task_hep_job_interference arr_seq sched j t =
hep_job j' j
        apply/idP/idP => [/hasP[j'' /[!mem_filter]/andP[RSERV IN] AHEP] | HEP].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
j'': Job
RSERV: receives_service_at sched j'' t
IN: j'' \in arrivals_up_to arr_seq t
AHEP: another_task_hep_job j'' j
hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model
  PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
another_task_hep_job_interference arr_seq sched j t
        -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
j'': Job
RSERV: receives_service_at sched j'' t
IN: j'' \in arrivals_up_to arr_seq t
AHEP: another_task_hep_job j'' j
hep_job j' j apply service_at_implies_scheduled_at in RSERV.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
j'': Job
RSERV: scheduled_at sched j'' t
IN: j'' \in arrivals_up_to arr_seq t
AHEP: another_task_hep_job j'' j
hep_job j' j
          have EQ: j' = j''; [by apply: H_uniprocessor_proc_model | subst j''].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
AHEP: another_task_hep_job j' j
IN: j' \in arrivals_up_to arr_seq t
RSERV: scheduled_at sched j' t
hep_job j' j
          by move: AHEP => /andP[].
        -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
another_task_hep_job_interference arr_seq sched j t apply/hasP; exists j'; [rewrite !mem_filter|]; apply/andP; split => //.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
receives_service_at sched j' t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model
  PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
j' \in arrivals_up_to arr_seq t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model
  PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
job_task j' != job_task j
          +
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
receives_service_at sched j' t by apply ideal_progress_inside_supplies => //.
          +
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
j' \in arrivals_up_to arr_seq t apply: arrived_between_implies_in_arrivals => //.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
arrived_between j' 0 t.+1
            apply/andP; split=> [//|].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
job_arrival j' < t.+1
            by apply H_jobs_must_arrive_to_execute in H_j'_sched; rewrite ltnS.
          +
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
job_task j' != job_task j by apply: contraNN H_j'_not_tsk => /eqP; rewrite /job_of_task => ->.
      Qed.

      (** Hence, if we assume that [j'] has higher-or-equal priority, ... *)
      Hypothesis H_j'_hep : hep_job j' j.

      (** ... we are able to show that [j] incurs higher-or-equal
          priority interference from another task. *)
      Lemma athep_interference_if :
        another_task_hep_job_interference arr_seq sched j t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
H_j'_hep: hep_job j' j
another_task_hep_job_interference arr_seq sched j t
      Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_not_tsk: ~~ job_of_task tsk j'
H_j'_sched: scheduled_at sched j' t
H_j'_hep: hep_job j' j
another_task_hep_job_interference arr_seq sched j t
        by rewrite athep_interference_iff.
      Qed.

    End FromDifferentTask.

    (** In the last subsection, we consider a case when the scheduled
        job [j'] has lower priority than job [j]. *)
    Section LowerPriority.

      (** Consider a job [j'] that has lower priority than job [j]
            and is scheduled at time instant [t].  *)
      Variable j' : Job.
      Hypothesis H_j'_sched : scheduled_at sched j' t.
      Hypothesis H_j'_lp : ~~ hep_job j' j.

      (** We prove that, in this case, there is no interference from
          higher-or-equal priority jobs at time [t]. *)
      Lemma no_ahep_interference_when_scheduled_lp :
        ~~ another_hep_job_interference arr_seq sched j t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_sched: scheduled_at sched j' t
H_j'_lp: ~~ hep_job j' j
~~ another_hep_job_interference arr_seq sched j t
      Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_sched: scheduled_at sched j' t
H_j'_lp: ~~ hep_job j' j
~~ another_hep_job_interference arr_seq sched j t
        apply/negP; move/hasP => [jlp /[!mem_filter]/andP[+ IN] AHEP].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_sched: scheduled_at sched j' t
H_j'_lp: ~~ hep_job j' j
jlp: Job
IN: jlp \in arrivals_up_to arr_seq t
AHEP: another_hep_job jlp j
receives_service_at sched jlp t -> False
        move/service_at_implies_scheduled_at => RSERV.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
j': Job
H_j'_sched: scheduled_at sched j' t
H_j'_lp: ~~ hep_job j' j
jlp: Job
IN: jlp \in arrivals_up_to arr_seq t
AHEP: another_hep_job jlp j
RSERV: scheduled_at sched jlp t
False
        have EQ: j' = jlp; [by apply: H_uniprocessor_proc_model | subst j'].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_supply: has_supply sched t
jlp: Job
H_j'_lp: ~~ hep_job jlp j
H_j'_sched: scheduled_at sched jlp t
IN: jlp \in arrivals_up_to arr_seq t
AHEP: another_hep_job jlp j
RSERV: scheduled_at sched jlp t
False
        by move: (H_j'_lp) AHEP => LP /andP [HEP A]; rewrite HEP in LP.
      Qed.

    End LowerPriority.

  End SupplyAndScheduledJob.

  (** In this section, we prove that the (abstract) cumulative
      interference of jobs with higher or equal priority is equal to
      total service of jobs with higher or equal priority. *)
  Section InstantiatedServiceEquivalences.

    (** First, let us assume that the introduced processor model is
          unit-service. *)
    Hypothesis H_unit_service : unit_service_proc_model PState.

    (** Consider any job [j] of [tsk]. *)
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.
    Hypothesis H_job_of_tsk : job_of_task tsk j.

    (** We consider an arbitrary time interval <<[t1, t)>> that starts
        with a (classic) quiet time. *)
    Variable t1 t : instant.
    Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.

    (** As follows from lemma [cumulative_pred_served_eq_service], the
        (abstract) instantiated function of interference is equal to
        the total service of any subset of jobs with higher or equal
        priority. *)

    (** The above is in particular true for the jobs other than [j]
        with higher or equal priority... *)
    Lemma  cumulative_i_ohep_eq_service_of_ohep :
      cumulative_another_hep_job_interference arr_seq sched j t1 t
      = service_of_other_hep_jobs arr_seq sched j t1 t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_unit_service: unit_service_proc_model PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
t1, t: instant
H_quiet_time: quiet_time arr_seq sched j t1
cumulative_another_hep_job_interference arr_seq sched
  j t1 t =
service_of_other_hep_jobs arr_seq sched j t1 t
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_unit_service: unit_service_proc_model PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
t1, t: instant
H_quiet_time: quiet_time arr_seq sched j t1
cumulative_another_hep_job_interference arr_seq sched
  j t1 t =
service_of_other_hep_jobs arr_seq sched j t1 t
      apply: cumulative_pred_served_eq_service => //.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_unit_service: unit_service_proc_model PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
t1, t: instant
H_quiet_time: quiet_time arr_seq sched j t1
forall j' : Job, another_hep_job j' j -> hep_job j' j
      -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_unit_service: unit_service_proc_model PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
t1, t: instant
H_quiet_time: quiet_time arr_seq sched j t1
forall j' : Job, another_hep_job j' j -> hep_job j' j by move => ? /andP[].
    Qed.

    (** ...and for jobs from other tasks than [j] with higher
        or equal priority. *)
    Lemma cumulative_i_thep_eq_service_of_othep :
      cumulative_another_task_hep_job_interference arr_seq sched j t1 t
      = service_of_other_task_hep_jobs arr_seq sched j t1 t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_unit_service: unit_service_proc_model PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
t1, t: instant
H_quiet_time: quiet_time arr_seq sched j t1
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 t =
service_of_other_task_hep_jobs arr_seq sched j t1 t
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_unit_service: unit_service_proc_model PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
t1, t: instant
H_quiet_time: quiet_time arr_seq sched j t1
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 t =
service_of_other_task_hep_jobs arr_seq sched j t1 t
      apply: cumulative_pred_served_eq_service => //.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_consumed_supply_proc_model: fully_consuming_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_unit_service: unit_service_proc_model PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
t1, t: instant
H_quiet_time: quiet_time arr_seq sched j t1
forall j' : Job,
another_task_hep_job j' j -> hep_job j' j
      by move => ? /andP[].
    Qed.

  End InstantiatedServiceEquivalences.

End InterferencePropertiesJLFP.