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]
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]
(** 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]
(** * Processor Executes HEP jobs at Preemption Point *) (** In this file, we show that, given a busy interval of a job [j], the processor is always busy scheduling a higher-or-equal-priority job at any preemptive point inside the busy interval. *) Section ProcessorBusyWithHEPJobAtPreemptionPoints. (** Consider any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{Arrival : JobArrival Job}. Context `{Cost : 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. (** ... and any ideal uniprocessor schedule of this arrival sequence. *) Variable sched : schedule (ideal.processor_state Job). (** Consider a JLFP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive and transitive. *) Context {JLFP : JLFP_policy Job}. Hypothesis H_priority_is_reflexive: reflexive_priorities. Hypothesis H_priority_is_transitive: transitive_priorities. (** In addition, we assume the existence of a function mapping a job and its progress to a boolean value saying whether this job is preemptable at its current point of execution. *) Context `{JobPreemptable Job}. (** Further, allow for any work-bearing notion of job readiness. *) Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}. Hypothesis H_job_ready : work_bearing_readiness arr_seq sched. (** We assume that the schedule is valid and that all jobs come from the arrival sequence. *) Hypothesis H_sched_valid : valid_schedule sched arr_seq. Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq. (** Next, we assume that the schedule is a work-conserving schedule... *) Hypothesis H_work_conserving : work_conserving arr_seq sched. (** ... and the schedule respects the scheduling policy at every preemption point. *) Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched JLFP. (** Consider any job [j] with positive job cost. *) Variable j : Job. Hypothesis H_j_arrives : arrives_in arr_seq j. Hypothesis H_job_cost_positive : job_cost_positive j. (** Consider any busy interval prefix <<[t1, t2)>> of job [j]. *) Variable t1 t2 : instant. Hypothesis H_busy_interval_prefix : busy_interval_prefix arr_seq sched j t1 t2. (** Consider an arbitrary preemption time t ∈ <<[t1,t2)>>. *) Variable t : instant. Hypothesis H_t_in_busy_interval : t1 <= t < t2. Hypothesis H_t_preemption_time : preemption_time sched t. (** First note since [t] lies inside the busy interval, the processor cannot be idle at time [t]. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

~ is_idle sched t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

~ is_idle sched t
by move => IDLE; exfalso; apply: not_quiet_implies_not_idle; rt_eauto. Qed. (** Next we consider two cases: (1) [t] is less than [t2 - 1] and (2) [t] is equal to [t2 - 1]. *) (** In case when [t < t2 - 1], we use the fact that time instant [t+1] is not a quiet time. The later implies that there is a pending higher-or-equal priority job at time [t]. Thus, the assumption that the schedule respects priority policy at preemption points implies that the scheduled job must have a higher-or-equal priority. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

t < t2.-1 -> forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

t < t2.-1 -> forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

t1 < t.+1 < t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
quiet_time arr_seq sched j t.+1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

t1 < t.+1 < t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

t1 < t.+1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
t.+1 < t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

t1 < t.+1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
t.+1 < t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

t.+1 < t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

t.+1 < t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LTt2m1: t + 1 < t2

t.+1 < t2
by rewrite -[t.+1]addn1.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

quiet_time arr_seq sched j t.+1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1

completed_by sched j_hp t.+1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1

pending sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1
PEND: pending sched j_hp t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1

pending sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1

has_arrived j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1
~~ completed_by sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1

has_arrived j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1
~~ completed_by sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1

~~ completed_by sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1

~~ completed_by sched j_hp t
by move: NCOMP'; apply contra, completion_monotonic.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1
PEND: pending sched j_hp t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP': hep_job j' j_hp

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j_hp: Job
ARR: arrives_in arr_seq j_hp
HP: hep_job j_hp j
BEF: arrived_before j_hp t.+1
NCOMP': ~~ completed_by sched j_hp t.+1
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP': hep_job j' j_hp
HEP: hep_job j' j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j

backlogged sched j' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
BACK: backlogged sched j' t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j

backlogged sched j' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j

~~ scheduled_at sched j' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
SCHED': scheduled_at sched j' t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
SCHED': scheduled_at sched j' t
EQ: jlp = j'

False
by subst; apply: NOTHP.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
BACK: backlogged sched j' t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
LTt2m1: t < t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
BACK: backlogged sched j' t

hep_job_at t jlp j'
by eapply H_respects_policy; eauto . Qed. (** In the case when [t = t2 - 1], we cannot use the same proof since [t+1 = t2], but [t2] is a quiet time. So we do a similar case analysis on the fact that [t1 = t ∨ t1 < t]. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

t = t2.-1 -> forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

t = t2.-1 -> forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
EQUALt1: t1 = t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
EQUALt1: t1 = t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1

job_arrival j = t2.-1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1
ARR: job_arrival j = t2.-1
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1

job_arrival j = t2.-1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1

t2.-1 <= job_arrival j <= t2.-1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
i: nat
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j i.+1.-1 i.+1
H_t_preemption_time: preemption_time sched i.+1.-1
H_t_in_busy_interval: i.+1.-1 <= i.+1.-1 < i.+1
jlp: Job
Sched_jlp: scheduled_at sched jlp i.+1.-1
NOTHP: ~ hep_job jlp j
INBI: i.+1.-1 <= job_arrival j < i.+1
NOTQUIET: forall t : nat, i.+1.-1 < t < i.+1 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j i.+1.-1

i.+1.-1 <= job_arrival j <= i.+1.-1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
i: nat
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j i.+1.-1 i.+1
H_t_preemption_time: preemption_time sched i.+1.-1
H_t_in_busy_interval: i.+1.-1 <= i.+1.-1 < i.+1
jlp: Job
Sched_jlp: scheduled_at sched jlp i.+1.-1
NOTHP: ~ hep_job jlp j
NOTQUIET: forall t : nat, i.+1.-1 < t < i.+1 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j i.+1.-1
INBI: i <= job_arrival j <= i

i.+1.-1 <= job_arrival j <= i.+1.-1
now rewrite -pred_Sn.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1
ARR: job_arrival j = t2.-1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1
ARR: job_arrival j = t2.-1
PEND: pending sched j t2.-1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1
ARR: job_arrival j = t2.-1
jhp: Job
ARRhp: arrives_in arr_seq jhp
PENDhp: job_ready sched jhp t2.-1
HEPhp: hep_job jhp j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1
ARR: job_arrival j = t2.-1
jhp: Job
ARRhp: arrives_in arr_seq jhp
PENDhp: job_ready sched jhp t2.-1
HEPhp: hep_job jhp j

hep_job_at 0 jlp jhp
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1
ARR: job_arrival j = t2.-1
jhp: Job
ARRhp: arrives_in arr_seq jhp
PENDhp: job_ready sched jhp t2.-1
HEPhp: hep_job jhp j

backlogged sched jhp t2.-1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1
ARR: job_arrival j = t2.-1
jhp: Job
ARRhp: arrives_in arr_seq jhp
PENDhp: job_ready sched jhp t2.-1
HEPhp: hep_job jhp j

~~ scheduled_at sched jhp t2.-1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1
ARR: job_arrival j = t2.-1
jhp: Job
ARRhp: arrives_in arr_seq jhp
PENDhp: job_ready sched jhp t2.-1
HEPhp: hep_job jhp j
SCHED: scheduled_at sched jhp t2.-1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t2.-1 t2
H_t_preemption_time: preemption_time sched t2.-1
H_t_in_busy_interval: t2.-1 <= t2.-1 < t2
jlp: Job
Sched_jlp: scheduled_at sched jlp t2.-1
NOTHP: ~ hep_job jlp j
INBI: t2.-1 <= job_arrival j < t2
NOTQUIET: forall t : nat, t2.-1 < t < t2 -> ~ quiet_time arr_seq sched j t
QUIET: quiet_time arr_seq sched j t2.-1
ARR: job_arrival j = t2.-1
jhp: Job
ARRhp: arrives_in arr_seq jhp
PENDhp: job_ready sched jhp t2.-1
HEPhp: hep_job jhp j
SCHED: scheduled_at sched jhp t2.-1
EQ: jhp = jlp

False
by subst; apply: NOTHP.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t

completed_by sched j_hp' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t

pending sched j_hp' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t
PEND: pending sched j_hp' t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t

pending sched j_hp' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t

has_arrived j_hp' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t
~~ completed_by sched j_hp' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t

has_arrived j_hp' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t
~~ completed_by sched j_hp' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t

~~ completed_by sched j_hp' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t

~~ completed_by sched j_hp' t
by move: NOTCOMP'; apply contra, completion_monotonic.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t
PEND: pending sched j_hp' t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP': hep_job j' j_hp'

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j_hp': Job
IN: arrives_in arr_seq j_hp'
HP: hep_job j_hp' j
ARR: arrived_before j_hp' t
NOTCOMP': ~~ completed_by sched j_hp' t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP': hep_job j' j_hp'
HEP: hep_job j' j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j

backlogged sched j' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
BACK: backlogged sched j' t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j

backlogged sched j' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j

~~ scheduled_at sched j' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
SCHED': scheduled_at sched j' t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
SCHED': scheduled_at sched j' t
EQ: jlp = j'

False
by subst; apply: NOTHP.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
BACK: backlogged sched j' t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
EQUALt2m1: t = t2.-1
jlp: Job
Sched_jlp: scheduled_at sched jlp t
NOTHP: ~ hep_job jlp j
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LARGERt1: t1 < t
j': Job
ARR': arrives_in arr_seq j'
READY': job_ready sched j' t
HEP: hep_job j' j
BACK: backlogged sched j' t

hep_job_at t jlp j'
by eapply H_respects_policy; eauto . } Qed. (** By combining the above facts we conclude that a job that is scheduled at time [t] has higher-or-equal priority. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

t <= t2.-1 -> forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
EQUALt2m1: t = t2.-1

forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LTt2m1: t < t2.-1
forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
EQUALt2m1: t = t2.-1

forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LTt2m1: t < t2.-1
forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LTt2m1: t < t2.-1

forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
GEt: t1 <= t
LEt: t < t2
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
LTt2m1: t < t2.-1

forall jhp : Job, scheduled_at sched jhp t -> hep_job jhp j
by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_lt. Qed. (** Since a job that is scheduled at time [t] has higher-or-equal priority, by properties of a busy interval it cannot arrive before time instant [t1]. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

forall jhp : Job, scheduled_at sched jhp t -> arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

forall jhp : Job, scheduled_at sched jhp t -> arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t

arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t

arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2

arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
HP: hep_job jhp j

arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
HP: hep_job jhp j
PENDING: scheduled_at sched jhp t

arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
HP: hep_job jhp j
PENDING: pending sched jhp t

arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
HP: hep_job jhp j
PENDING: pending sched jhp t

t1 <= job_arrival jhp
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
HP: hep_job jhp j
PENDING: pending sched jhp t
LT: job_arrival jhp < t1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: hep_job jhp j -> arrived_before jhp t1 -> completed_by sched jhp t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
HP: hep_job jhp j
PENDING: pending sched jhp t
LT: job_arrival jhp < t1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: completed_by sched jhp t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
HP: hep_job jhp j
PENDING: pending sched jhp t
LT: job_arrival jhp < t1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: completed_by sched jhp t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
HP: hep_job jhp j
PENDING: pending sched jhp t
LT: job_arrival jhp < t1
COMP: completed_by sched jhp t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
CONS: jobs_come_from_arrival_sequence sched arr_seq
WORK: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
jhp: Job
Sched_jhp: scheduled_at sched jhp t
SL: t1 < t2
QUIET: completed_by sched jhp t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
HP: hep_job jhp j
PENDING: pending sched jhp t
LT: job_arrival jhp < t1
COMP: ~~ scheduled_at sched jhp t

False
by move: COMP => /negP COMP; apply COMP. Qed. (** From the above lemmas we prove that there is a job [jhp] that is (1) scheduled at time [t], (2) has higher-or-equal priority, and (3) arrived between [t1] and [t2]. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

exists j_hp : Job, arrived_between j_hp t1 t2 /\ hep_job j_hp j /\ scheduled_at sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t

exists j_hp : Job, arrived_between j_hp t1 t2 /\ hep_job j_hp j /\ scheduled_at sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2

exists j_hp : Job, arrived_between j_hp t1 t2 /\ hep_job j_hp j /\ scheduled_at sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2

exists j_hp : Job, arrived_between j_hp t1 t2 /\ hep_job j_hp j /\ scheduled_at sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
Idle: is_idle sched t

exists j_hp : Job, arrived_between j_hp t1 t2 /\ hep_job j_hp j /\ scheduled_at sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t
exists j_hp : Job, arrived_between j_hp t1 t2 /\ hep_job j_hp j /\ scheduled_at sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
Idle: is_idle sched t

exists j_hp : Job, arrived_between j_hp t1 t2 /\ hep_job j_hp j /\ scheduled_at sched j_hp t
by exfalso; apply instant_t_is_not_idle.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t

exists j_hp : Job, arrived_between j_hp t1 t2 /\ hep_job j_hp j /\ scheduled_at sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t

arrived_between jhp t1 t2 /\ hep_job jhp j /\ scheduled_at sched jhp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t

arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t
hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t
scheduled_at sched jhp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t

arrived_between jhp t1 t2
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t
hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t
scheduled_at sched jhp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t

hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t
scheduled_at sched jhp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t

hep_job jhp j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t
scheduled_at sched jhp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t

scheduled_at sched jhp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (processor_state Job)
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
H: JobPreemptable Job
H0: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched JLFP
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_interval_prefix: busy_interval_prefix arr_seq sched j t1 t2
t: instant
H_t_in_busy_interval: t1 <= t < t2
H_t_preemption_time: preemption_time sched t
SL: t1 < t2
QUIET: quiet_time arr_seq sched j t1
NOTQUIET: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
INBI: t1 <= job_arrival j < t2
GEt: t1 <= t
LEt: t < t2
jhp: Job
Sched_jhp: scheduled_at sched jhp t

scheduled_at sched jhp t
by done. Qed. End ProcessorBusyWithHEPJobAtPreemptionPoints.