Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
(** Throughout this file, we assume ideal uni-processor schedules. *)
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** * Lemmas about Priority Inversion for ideal uni-processors *) (** In this section, we prove a few useful properties about the notion of priority inversion for ideal uni-processors. *) Section PIIdealProcessorModelLemmas. (** 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 arrival sequence with consistent arrivals. *) Variable arr_seq : arrival_sequence Job. Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq. (** Next, consider any ideal uni-processor schedule of this arrival sequence ... *) Variable sched : schedule (ideal.processor_state Job). 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. (** Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive. *) Context `{JLFP_policy Job}. Hypothesis H_priority_is_reflexive : reflexive_priorities. (** Let [tsk] be any task to be analyzed. *) Variable tsk : Task. (** Consider a job [j] of task [tsk]. In this subsection, job [j] is deemed to be the main job with respect to which the priority inversion is computed. *) Variable j : Job. Hypothesis H_j_tsk : job_of_task tsk j. (** Consider a time instant [t]. *) Variable t : instant. (** We prove that if the processor is idle at time [t], then there is no priority inversion. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant

is_idle sched t -> priority_inversion_dec arr_seq sched j t = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant

is_idle sched t -> priority_inversion_dec arr_seq sched j t = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
IDLE: is_idle sched t

~~ scheduled_at sched j t && has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
IDLE: is_idle sched t

~~ has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
IDLE: is_idle sched t
s: Job
IN: s \in arrivals_before arr_seq t.+1

~~ (scheduled_at sched s t && ~~ hep_job s j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
IDLE: is_idle sched t
s: Job
IN: s \in arrivals_before arr_seq t.+1

~~ scheduled_at sched s t
by move: IDLE => /eqP; rewrite scheduled_at_def => ->. Qed. (** Next, consider an additional job [j'] and assume it is scheduled at time [t]. *) Variable j' : Job. Hypothesis H_j'_sched : scheduled_at sched j' t. (** Then, we prove that from point of view of job [j], priority inversion appears iff [s] has lower priority than job [j]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t

priority_inversion_dec 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
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t

priority_inversion_dec 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
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t

~~ scheduled_at sched j t && has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = true

false = ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = true

false = ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = true
EQ: j = j'

false = ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
H_j'_sched: scheduled_at sched j t
SCHED2: scheduled_at sched j t = true

hep_job j j
by apply (H_priority_is_reflexive 0).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false

has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false

has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = true

has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = true
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = true

has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = true
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = true
l: Job
IN: l \in arrivals_before arr_seq t.+1

~~ (scheduled_at sched l t && ~~ hep_job l j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = true
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = true
l: Job
IN: l \in arrivals_before arr_seq t.+1
SCHED3: scheduled_at sched l t = true

~~ ~~ hep_job l j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = true
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = true
l: Job
IN: l \in arrivals_before arr_seq t.+1
SCHED3: scheduled_at sched l t = true
EQ: l = j'

~~ ~~ hep_job l j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = true
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false

has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = true
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false

has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1) = true
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false

j' \in arrivals_before arr_seq t.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false
scheduled_at sched j' t && ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
SCHED2: scheduled_at sched j t = false
HEP: hep_job j' j = false

scheduled_at sched j' t && ~~ hep_job j' j
by rewrite H_j'_sched HEP. } Qed. (** Assume that [j'] has higher-or-equal priority than job [j], then we prove that there is no priority inversion for job [j]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t

hep_job j' j -> priority_inversion_dec arr_seq sched j t = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t

hep_job j' j -> priority_inversion_dec arr_seq sched j t = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j

priority_inversion_dec arr_seq sched j t = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
HEP: hep_job j' j
NSCHED: ~~ scheduled_at sched j t
j'': Job
SCHED: scheduled_at sched j'' t
PRIO: ~~ hep_job j'' j

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j'': Job
HEP: hep_job j'' j
H_j'_sched: scheduled_at sched j'' t
NSCHED: ~~ scheduled_at sched j t
SCHED: scheduled_at sched j'' t
PRIO: ~~ hep_job j'' j

False
by rewrite HEP in PRIO. Qed. (** Assume that [j'] has lower priority than job [j], then we prove that [j] incurs priority inversion. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t

~~ hep_job j' j -> priority_inversion_dec arr_seq sched j t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t

~~ hep_job j' j -> priority_inversion_dec arr_seq sched j t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

priority_inversion_dec arr_seq sched j t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

~~ scheduled_at sched j t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

~~ scheduled_at sched j t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
SCHED: scheduled_at sched j t

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
LP: ~~ hep_job j j
H_j'_sched, SCHED: scheduled_at sched j t

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
LP: ~~ hep_job j j
H_j'_sched, SCHED: scheduled_at sched j t

hep_job j j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive (T:=Job) (hep_job_at 0)
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
LP: ~~ hep_job j j
H_j'_sched, SCHED: scheduled_at sched j t

hep_job j j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive (T:=Job) (fun j1 : Job => [eta hep_job j1])
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
LP: ~~ hep_job j j
H_j'_sched, SCHED: scheduled_at sched j t

hep_job j j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

has (fun jlp : Job => scheduled_at sched jlp t && ~~ hep_job jlp j) (arrivals_before arr_seq t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

exists2 x : Job, x \in arrivals_before arr_seq t.+1 & scheduled_at sched x t && ~~ hep_job x j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

j' \in arrivals_before arr_seq t.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
scheduled_at sched j' t && ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

j' \in arrivals_before arr_seq t.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
scheduled_at sched j' t && ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

arrived_between j' 0 t.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
scheduled_at sched j' t && ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

job_arrival j' < t.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j
scheduled_at sched j' t && ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

scheduled_at sched j' t && ~~ hep_job j' j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
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
H3: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
tsk: Task
j: Job
H_j_tsk: job_of_task tsk j
t: instant
j': Job
H_j'_sched: scheduled_at sched j' t
LP: ~~ hep_job j' j

scheduled_at sched j' t && ~~ hep_job j' j
by apply/andP; split. Qed. End PIIdealProcessorModelLemmas.