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]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** In this section, we prove some fundamental properties of the FIFO policy. *) Section BasicLemmas. (** We assume the basic (i.e., Liu & Layland) readiness model under which any pending job is ready. *) #[local] Existing Instance basic_ready_instance. (** Consider any type of jobs with arrival times and execution costs. *) Context `{Job : JobType} {Arrival : JobArrival Job} {Cost : JobCost Job}. (** Consider any arrival sequence of such jobs ... *) Variable arr_seq : arrival_sequence Job. (** ... and the resulting ideal uniprocessor schedule. We assume that the schedule is valid and work-conserving. *) Variable sched : schedule (ideal.processor_state Job). Hypothesis H_schedule_is_valid : valid_schedule sched arr_seq. Hypothesis H_work_conservation : work_conserving arr_seq sched. (** Suppose jobs have preemption points ... *) Context `{JobPreemptable Job}. (** ...and that the preemption model is valid. *) Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched. (** Assume that the schedule respects the FIFO scheduling policy whenever jobs are preemptable. *) Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job). (** We observe that there is no priority inversion in a FIFO-compliant schedule. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)

forall (j : Job) (t : instant), arrives_in arr_seq j -> pending sched j t -> ~ priority_inversion sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)

forall (j : Job) (t : instant), arrives_in arr_seq j -> pending sched j t -> ~ priority_inversion sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
ARRIVED: has_arrived j t
NCOMPL: ~ completed_by sched j t
NSCHED: ~~ scheduled_at sched j t
jlp: Job
SCHED: scheduled_at sched jlp t
PRIO: ~~ hep_job jlp j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
ARRIVED: has_arrived j t
NCOMPL: ~ completed_by sched j t
NSCHED: ~~ scheduled_at sched j t
jlp: Job
SCHED: scheduled_at sched jlp t
LT: job_arrival j < job_arrival jlp

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
ARRIVED: has_arrived j t
NSCHED: ~~ scheduled_at sched j t
jlp: Job
SCHED: scheduled_at sched jlp t
LT: job_arrival j < job_arrival jlp

always_higher_priority j jlp
by intros t'; apply/andP; split; unfold hep_job_at, JLFP_to_JLDP, hep_job, FIFO; lia. Qed. (** In this section, we prove the cumulative priority inversion for any task is bounded by [0]. *) Section PriorityInversionBounded. (** Consider any kind of tasks. *) Context `{Task : TaskType} `{JobTask Job Task}. (** Consider a task [tsk]. *) Variable tsk : Task. (** Assume the arrival times are consistent. *) Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq. (** Assume that the schedule follows the FIFO policy at preemption time. *) Hypothesis H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job). (** Assume the schedule is valid. *) Hypothesis H_valid_schedule : valid_schedule sched arr_seq. (** Assume there are no duplicates in the arrival sequence. *) Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq. (** Then we prove that the amount of priority inversion is bounded by 0. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq

priority_inversion_is_bounded_by_constant arr_seq sched tsk 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq

priority_inversion_is_bounded_by_constant arr_seq sched tsk 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2

cumulative_priority_inversion arr_seq sched j t1 t2 <= 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2

\sum_(t1 <= t < t2) priority_inversion_dec arr_seq sched j t <= 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2

\sum_(t1 <= t < t2) priority_inversion_dec arr_seq sched j t = 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2

priority_inversion_dec arr_seq sched j t = 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2

~~ priority_inversion_dec arr_seq sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
INV: jobs_come_from_arrival_sequence sched arr_seq -> jobs_must_arrive_to_execute sched -> consistent_arrival_times arr_seq -> priority_inversion sched j t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
INV: priority_inversion sched j t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LP: ~~ hep_job j__lp j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp

completed_by sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp

completed_by sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp

always_higher_priority j j__lp
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
t': instant

(job_arrival j <= job_arrival j__lp) && (job_arrival j < job_arrival j__lp)
by apply/andP; split; first apply ltnW.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
BUSY: busy_interval_prefix arr_seq sched j t1 t2
t: nat
T1: t1 <= t
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
t: nat
T1: t1 <= t
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
NQT: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
t: nat
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
NQT: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
EQ: t1 = t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
t: nat
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
NQT: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
GT: t1 < t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
t: nat
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
NQT: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
EQ: t1 = t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
NSCHED: ~~ scheduled_at sched j t1
T2: t1 < t2
j__lp: Job
SCHED: scheduled_at sched j__lp t1
LT: job_arrival j < job_arrival j__lp
COMPL: exists t' : nat, job_arrival j <= t' < t1 /\ scheduled_at sched j t'
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
NQT: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

False
by case: COMPL => [t' [/andP [ARR3 LT__temp] SCHED__temp]]; lia.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
t: nat
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
NQT: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
GT: t1 < t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
t: nat
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
NQT: forall t : nat, t1 < t < t2 -> ~ quiet_time arr_seq sched j t
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
GT: t1 < t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
t: nat
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
GT: t1 < t

quiet_time arr_seq sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
t: nat
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
GT: t1 < t
j_hp: Job
ARR: arrives_in arr_seq j_hp
ARRB: arrived_before j_hp t
HEP: job_arrival j_hp <= job_arrival j

completed_by sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
tsk: Task
H_consistent_arrival_times: consistent_arrival_times arr_seq
H_respects_policy_at_preemption_point: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_valid_schedule: valid_schedule sched arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
ARRIN: arrives_in arr_seq j
TASK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
t: nat
T2: t < t2
NSCHED: ~~ scheduled_at sched j t
j__lp: Job
SCHED: scheduled_at sched j__lp t
LT: job_arrival j < job_arrival j__lp
COMPL: completed_by sched j t
LE: t1 < t2
QT: quiet_time arr_seq sched j t1
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
GT: t1 < t
j_hp: Job
ARR: arrives_in arr_seq j_hp
ARRB: arrived_before j_hp t
HEP: job_arrival j_hp <= job_arrival j

always_higher_priority j_hp j__lp
by move => t'; apply/andP; split; rewrite /hep_job_at /FIFO /JLFP_to_JLDP /hep_job //=; lia. } Qed. End PriorityInversionBounded. (** We prove that in a FIFO-compliant schedule, if a job [j] is scheduled, then all jobs with higher priority than [j] have been completed. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)

forall (j : Job) (t : instant), scheduled_at sched j t -> forall j_hp : Job, arrives_in arr_seq j_hp -> ~~ hep_job j j_hp -> completed_by sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)

forall (j : Job) (t : instant), scheduled_at sched j t -> forall j_hp : Job, arrives_in arr_seq j_hp -> ~~ hep_job j j_hp -> completed_by sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp

completed_by sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'

completed_by sched j_hp t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'

scheduled_at sched j' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'

scheduled_at sched j' t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'
transitive_priorities
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'
work_bearing_readiness arr_seq sched
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'
valid_schedule sched arr_seq
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'
valid_preemption_model arr_seq sched
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'
respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'
arrives_in arr_seq j_hp
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'
job_arrival j_hp < job_arrival j'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'
always_higher_priority j_hp j'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'

always_higher_priority j_hp j'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j': Job
t: instant
SCHED: scheduled_at sched j' t
j_hp: Job
ARRjhp: arrives_in arr_seq j_hp
HEP: ~~ hep_job j' j_hp
EARLIER: job_arrival j_hp < job_arrival j'
t': instant

hep_job_at t' j_hp j'
by apply ltnW. Qed. (** The next lemma considers FIFO schedules in the context of tasks. *) Section SequentialTasks. (** If the scheduled jobs stem from a set of tasks, ... *) Context {Task : TaskType}. Context `{JobTask Job Task}. (** ... then the tasks in a FIFO-compliant schedule necessarily execute sequentially. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task

sequential_tasks arr_seq sched
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task

sequential_tasks arr_seq sched
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
j1, j2: Job
t: instant
ARRj1: arrives_in arr_seq j1
ARRj2: arrives_in arr_seq j2
SAME_TASKx: same_task j1 j2
LT: job_arrival j1 < job_arrival j2

scheduled_at sched j2 t -> completed_by sched j1 t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task
j1, j2: Job
t: instant
ARRj1: arrives_in arr_seq j1
ARRj2: arrives_in arr_seq j2
SAME_TASKx: same_task j1 j2
LT: job_arrival j1 < job_arrival j2

always_higher_priority j1 j2
by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=]. Qed. (** We also note that the [FIFO] policy respects sequential tasks. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task

policy_respects_sequential_tasks
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
Task: TaskType
H0: JobTask Job Task

policy_respects_sequential_tasks
by move => j1 j2 SAME ARRLE; rewrite /hep_job /FIFO. Qed. End SequentialTasks. (** Finally, let us further assume that there are no needless preemptions among jobs of equal priority. *) Hypothesis H_no_superfluous_preemptions : no_superfluous_preemptions sched. (** In the absence of superfluous preemptions and under assumption of the basic readiness model, there are no preemptions at all in a FIFO-compliant schedule. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched

forall (j : Job) (t : instant), ~~ preempted_at sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched

forall (j : Job) (t : instant), ~~ preempted_at sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant

~~ preempted_at sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant

~ preempted_at sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant
CONTR: preempted_at sched j t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
s: Job
INTER: scheduled_at sched s t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t

backlogged sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t
j_other: Job
SCHEDj_other: scheduled_at sched j_other t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t

backlogged sched j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t
j_other: Job
SCHEDj_other: scheduled_at sched j_other t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t

has_arrived j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t
j_other: Job
SCHEDj_other: scheduled_at sched j_other t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t
SCHED1: pending sched j t.-1

has_arrived j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t
j_other: Job
SCHEDj_other: scheduled_at sched j_other t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t
HAS: has_arrived j t.-1
COMPL: ~~ completed_by sched j t.-1

has_arrived j t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t
j_other: Job
SCHEDj_other: scheduled_at sched j_other t
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t
j_other: Job
SCHEDj_other: scheduled_at sched j_other t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
IDLE: ideal.is_idle sched t
j_other: Job
SCHEDj_other: scheduled_at sched j_other t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
j_other: Job

scheduled_at sched j_other t -> ideal.is_idle sched t -> False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
j: Job
t: instant
H_work_conservation: arrives_in arr_seq j -> backlogged sched j t -> exists j_other : Job, scheduled_at sched j_other t
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
j_other: Job
SCHED: sched t = Some j_other
IDLE: sched t = None

False
by rewrite IDLE in SCHED.
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
s: Job
INTER: scheduled_at sched s t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched
j: Job
t: instant
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
s: Job
INTER: scheduled_at sched s t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t

~~ hep_job j s
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: ~~ hep_job j s
False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t

~~ hep_job j s
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t

preempted_at sched j t
by repeat (apply /andP ; split; try by done).
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: ~~ hep_job j s

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: job_arrival s < job_arrival j

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: job_arrival s < job_arrival j
SCHED1: completed_by sched s t.-1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: job_arrival s < job_arrival j
always_higher_priority s j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: job_arrival s < job_arrival j
SCHED1: completed_by sched s t.-1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: job_arrival s < job_arrival j
always_higher_priority s j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: ~~ completed_by sched s t
HEP: job_arrival s < job_arrival j
SCHED1: completed_by sched s t.-1

False
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: job_arrival s < job_arrival j
always_higher_priority s j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: job_arrival s < job_arrival j

always_higher_priority s j
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
j: Job
t: instant
s: Job
H_no_superfluous_preemptions: preempted_at sched j t -> scheduled_at sched s t -> ~~ hep_job_at t j s
SCHED1: scheduled_at sched j t.-1
NCOMPL: ~~ completed_by sched j t
SCHED2: ~~ scheduled_at sched j t
COME: jobs_come_from_arrival_sequence sched arr_seq
MUST: jobs_must_be_ready_to_execute sched
INTER: scheduled_at sched s t
HEP: job_arrival s < job_arrival j

always_higher_priority s j
by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=]. } Qed. (** It immediately follows that FIFO schedules are non-preemptive. *)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched

nonpreemptive_schedule sched
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_is_valid: valid_schedule sched arr_seq
H_work_conservation: work_conserving arr_seq sched
H: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job)
H_no_superfluous_preemptions: no_superfluous_preemptions sched

nonpreemptive_schedule sched
by rewrite -no_preemptions_equiv_nonpreemptive; apply no_preemptions_under_FIFO. Qed. End BasicLemmas. (** We add the following lemmas to the basic facts database *) Global Hint Resolve fifo_respects_sequential_tasks tasks_execute_sequentially : basic_rt_facts.