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]
Require Export prosa.util.list. (** * Correctness of the work-conservation transformation *) (** This file contains the main argument of the work-conservation proof, starting with an analysis of the individual functions that drive the work-conservation transformation of a given reference schedule and ending with the proofs of individual properties of the obtained work-conserving schedule. *) (** In order to discuss the correctness of the work-conservation transformation at a high level, we first need a set of lemmas about the inner parts of the procedure. *) Section AuxiliaryLemmasWorkConservingTransformation. (** We assume ideal uni-processor schedules. *) #[local] Existing Instance ideal.processor_state. (** 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, costs, and deadlines... *) Context {Job : JobType}. Context `{JobArrival Job}. Context `{JobCost Job}. Context `{JobDeadline Job}. (** ...and an arbitrary arrival sequence. *) Variable arr_seq: arrival_sequence Job. Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq. (** We introduce the notion of work-conservation at a given time [t]. The definition is based on the concept of readiness of a job, and states that the presence of a ready job implies that the processor is not idle. *) Definition is_work_conserving_at sched t := (exists j, arrives_in arr_seq j /\ job_ready sched j t) -> exists j, sched t = Some j. (** First, we prove some useful properties about the most fundamental operation of the work-conservation transformation: swapping two processor states [t1] and [fsc], with [fsc] being a valid swap candidate of [t1]. *) Section JobsMustBeReadyFindSwapCandidate. (** Consider an ideal uniprocessor schedule... *) Variable sched: schedule (ideal.processor_state Job). (** ...in which jobs must be ready to execute. *) Hypothesis H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched. (** Consider an arbitrary time instant [t1]. *) Variable t1: instant. (** Let us define [fsc] as the result of the search for a swap candidate starting from [t1]... *) Let fsc := find_swap_candidate arr_seq sched t1. (** ...and [sched'] as the schedule resulting from the swap. *) Let sched' := swapped sched t1 fsc. (** First, we show that, in any case, the result of the search will yield an instant that is in the future (or, in case of failure, equal to [t1]). *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)

t1 <= fsc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)

t1 <= fsc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)

t1 <= match search_arg sched (relevant_pstate t1) (fun=> xpred0) t1 (max_deadline_for_jobs_arrived_before arr_seq t1) with | Some t_swap => t_swap | None => t1 end
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
n: nat
search_result: search_arg sched (relevant_pstate t1) (fun=> xpred0) t1 (max_deadline_for_jobs_arrived_before arr_seq t1) = Some n

t1 <= n
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
n: nat
search_result: t1 <= n < max_deadline_for_jobs_arrived_before arr_seq t1

t1 <= n
by move:search_result => /andP [LEQ LMAX]. Qed. (** Also, we show that the search will not yield jobs that arrive later than the given reference time. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)

forall (j : Job) (t : instant), sched (find_swap_candidate arr_seq sched t) == Some j -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)

forall (j : Job) (t : instant), sched (find_swap_candidate arr_seq sched t) == Some j -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant

sched (find_swap_candidate arr_seq sched t) == Some j -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant

sched match search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) with | Some t_swap => t_swap | None => t end == Some j -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = None

sched t == Some j -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
n: nat
RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = Some n
sched n == Some j -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = None

sched t == Some j -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = None
sched_j: scheduled_in j (sched t)

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = None
sched_j: scheduled_in j (sched t)

job_ready sched j t
exact: job_scheduled_implies_ready.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
n: nat
RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = Some n

sched n == Some j -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
n: nat
RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = Some n

sched n == Some j -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
n: nat
RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = Some n
SCHED_J: sched n = Some j

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
n: nat
SCHED_J: sched n = Some j

relevant_pstate t (sched n) -> has_arrived j t
rewrite SCHED_J //. } Qed. (** Next, we extend the previous lemma by stating that no job in the transformed schedule is scheduled before its arrival. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)

jobs_must_arrive_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)

jobs_must_arrive_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
OTHER: scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
AT_T1: t = t1 /\ scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j fsc
has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
AT_T2: t = fsc /\ scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
OTHER: scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
OTHER: scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t

job_ready sched j t
by apply: job_scheduled_implies_ready; rewrite // -OTHER.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
AT_T1: t = t1 /\ scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j fsc

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
AT_T2: t = fsc /\ scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
AT_T1: t = t1 /\ scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j fsc

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
AT_T1: t = t1 /\ scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j fsc

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T1: t = t1
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j fsc

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T1: t = t1
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j fsc

sched (find_swap_candidate arr_seq sched t) == Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T1: t = t1
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j fsc

scheduled_at sched' j t -> sched (find_swap_candidate arr_seq sched t) == Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T1: t = t1
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j fsc

scheduled_at (swapped sched t1 fsc) j t1 -> sched t2 == Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T1: t = t1
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t1 = scheduled_at sched j fsc

scheduled_at (swapped sched t1 fsc) j t1 -> sched t2 == Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T1: t = t1
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t1 = scheduled_at sched j fsc

scheduled_in j (sched fsc) -> sched t2 == Some j
by rewrite scheduled_in_def.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
AT_T2: t = fsc /\ scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
AT_T2: t = fsc /\ scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T2: t = fsc
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T2: t = fsc
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
ORDER: t1 <= t2

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T2: t = fsc
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
ORDER: t1 <= t2

job_ready sched j t1
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T2: t = fsc
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
ORDER: t1 <= t2
READY: job_ready sched j t1
has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T2: t = fsc
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
ORDER: t1 <= t2

job_ready sched j t1
by apply: job_scheduled_implies_ready; rewrite // -SCHED_AT'.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T2: t = fsc
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
ORDER: t1 <= t2
READY: job_ready sched j t1

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T2: t = fsc
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
ORDER: t1 <= t2
READY: has_arrived j t1 && ~~ (job_cost j <= service sched j t1)

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T2: t = fsc
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
ORDER: t1 <= t2
ARR: has_arrived j t1

has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
EQ_T2: t = fsc
SCHED_AT': scheduled_at (swapped sched t1 fsc) j t = scheduled_at sched j t1
ORDER: t1 <= t2
ARR: has_arrived j t1

has_arrived j fsc
exact: (leq_trans ARR). Qed. (** Finally we show that, in the transformed schedule, jobs are scheduled only if they are ready. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)

jobs_must_be_ready_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)

jobs_must_be_ready_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t

job_ready sched' j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t

job_ready (swapped sched t1 fsc) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

job_ready (swapped sched t1 fsc) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

has_arrived j t && ~~ completed_by (swapped sched t1 fsc) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

~~ completed_by (swapped sched t1 fsc) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

service (swapped sched t1 fsc) j t < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

t1 <= fsc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
unit_service_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
ideal_progress_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
completed_jobs_dont_execute sched
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

t1 <= fsc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
unit_service_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
ideal_progress_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
completed_jobs_dont_execute sched
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

unit_service_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
ideal_progress_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
completed_jobs_dont_execute sched
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

unit_service_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
ideal_progress_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
completed_jobs_dont_execute sched
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

ideal_progress_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
completed_jobs_dont_execute sched
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

ideal_progress_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat
completed_jobs_dont_execute sched
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

completed_jobs_dont_execute sched
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched
t1: instant
fsc:= find_swap_candidate arr_seq sched t1: nat
sched':= swapped sched t1 fsc: schedule (processor_state Job)
j: Job
t: instant
SCHED_AT: scheduled_at sched' j t
t2:= find_swap_candidate arr_seq sched t1: nat

completed_jobs_dont_execute sched
by eapply completed_jobs_are_not_ready. Qed. End JobsMustBeReadyFindSwapCandidate. (** In the following section, we put our attention on the point-wise transformation performed at each point in time prior to the horizon. *) Section MakeWCAtFacts. (** Consider an ideal uniprocessor schedule... *) Variable sched: schedule (ideal.processor_state Job). (** ...and take an arbitrary point in time... *) Variable t: instant. (** ...we define [sched'] as the resulting schedule after one point-wise transformation. *) Let sched' := make_wc_at arr_seq sched t. (** We start by proving that the point-wise transformation can only lead to higher service for a job at a given time. This is true because we swap only idle processor states with ones in which a job is scheduled. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

forall (j : Job) (t : instant), service sched j t <= service sched' j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

forall (j : Job) (t : instant), service sched j t <= service sched' j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant

service sched j t' <= service sched' j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant

service sched j t' <= service match sched t with | Some _ => sched | None => swapped sched t (find_swap_candidate arr_seq sched t) end j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None

service sched j t' <= service (swapped sched t (find_swap_candidate arr_seq sched t)) j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat

service sched j t' <= service (swapped sched t t2) j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat
ORDER: t <= find_swap_candidate arr_seq sched t

service sched j t' <= service (swapped sched t t2) j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat
ORDER: t <= find_swap_candidate arr_seq sched t
BOUND1: t < t'

service sched j t' <= service (swapped sched t t2) j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat
ORDER: t <= find_swap_candidate arr_seq sched t
BOUND1: t < t'
BOUND2: t' <= t2

service sched j t' <= service (swapped sched t t2) j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat
ORDER: t <= find_swap_candidate arr_seq sched t
BOUND1: t < t'
BOUND2: t' <= t2
SCHED_AT_T1: scheduled_at sched j t = false

service sched j t' <= service (swapped sched t t2) j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat
ORDER: t <= find_swap_candidate arr_seq sched t
BOUND1: t < t'
BOUND2: t' <= t2
NOT_AT_t1: ~~ scheduled_at sched j t

service sched j t' <= service (swapped sched t t2) j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat
ORDER: t <= find_swap_candidate arr_seq sched t
BOUND1: t < t'
BOUND2: t' <= t2
NOT_AT_t1: ~~ scheduled_at sched j t
SCHED_AT_T2: scheduled_at sched j t2 = true

service sched j t' <= service (swapped sched t t2) j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat
ORDER: t <= find_swap_candidate arr_seq sched t
BOUND1: t < t'
BOUND2: t' <= t2
NOT_AT_t1: ~~ scheduled_at sched j t
SCHED_AT_T2: scheduled_at sched j t2 = true

service_during sched j 0 t' <= service_during (replace_at sched t (sched t2)) j 0 t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat
ORDER: t <= find_swap_candidate arr_seq sched t
BOUND1: t < t'
BOUND2: t' <= t2
NOT_AT_t1: ~~ scheduled_at sched j t
SCHED_AT_T2: scheduled_at sched j t2 = true

service_during sched j 0 t' <= service_during sched j 0 t' + service_at (replace_at sched t (sched t2)) j t - service_at sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
PSTATE: sched t = None
t2:= find_swap_candidate arr_seq sched t: nat
ORDER: t <= find_swap_candidate arr_seq sched t
BOUND1: t < t'
BOUND2: t' <= t2
NOT_AT_t1: ~~ scheduled_at sched j t
SCHED_AT_T2: scheduled_at sched j t2 = true

service_during sched j 0 t' <= service_during sched j 0 t' + service_at (replace_at sched t (sched t2)) j t
by apply leq_addr. Qed. (** Next, we show that any ready job in the transformed schedule must be ready also in the original one, since the transformation can only lead to higher service. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

forall (j : Job) (t : instant), job_ready sched' j t -> job_ready sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

forall (j : Job) (t : instant), job_ready sched' j t -> job_ready sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant

job_ready sched' j t' -> job_ready sched j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant

has_arrived j t' && ~~ completed_by sched' j t' -> has_arrived j t' && ~~ completed_by sched j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
ARR: has_arrived j t'
COMP_BY: ~~ completed_by sched' j t'

has_arrived j t' && ~~ completed_by sched j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
ARR: has_arrived j t'
COMP_BY: ~~ completed_by sched' j t'

~~ completed_by sched j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
ARR: has_arrived j t'

completed_by sched j t' -> completed_by sched' j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
ARR: has_arrived j t'

job_cost j <= service sched j t' -> job_cost j <= service sched' j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
ARR: has_arrived j t'
LEQ: service sched j t' <= service sched' j t'

job_cost j <= service sched j t' -> job_cost j <= service sched' j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': instant
ARR: has_arrived j t'

job_cost j <= service sched j t' -> service sched j t' <= service sched' j t' -> job_cost j <= service sched' j t'
by apply leq_trans. Qed. (** Since the search for a swap candidate is performed until the latest deadline among all the jobs arrived before the reference time, we need to show that the computed deadline is indeed the latest. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

forall (j : Job) (t : nat), arrives_in arr_seq j -> job_arrival j <= t -> job_deadline j <= max_deadline_for_jobs_arrived_before arr_seq t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

forall (j : Job) (t : nat), arrives_in arr_seq j -> job_arrival j <= t -> job_deadline j <= max_deadline_for_jobs_arrived_before arr_seq t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': nat
ARR_IN: arrives_in arr_seq j
ARR: job_arrival j <= t'

job_deadline j <= max_deadline_for_jobs_arrived_before arr_seq t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': nat
ARR_IN: arrives_in arr_seq j
ARR: job_arrival j <= t'

job_deadline j <= max0 [seq job_deadline i | i <- arrivals_up_to arr_seq t']
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': nat
ARR_IN: arrives_in arr_seq j
ARR: job_arrival j <= t'

j \in arrivals_up_to arr_seq t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
t': nat
ARR_IN: arrives_in arr_seq j
ARR: job_arrival j <= t'

j \in arrivals_between arr_seq 0 t'.+1
apply arrived_between_implies_in_arrivals; by move:H_arr_seq_valid => [CONS UNIQ]. Qed. (** Next, we want to show that, if a job arriving from the arrival sequence is ready at some instant, then the point-wise transformation is guaranteed to find a job to swap with. We will proceed by doing a case analysis, and show that it is impossible that a swap candidate is not found. *) Section MakeWCAtFindsReadyJobs. (** We need to assume that, in the original schedule, all the deadlines of the jobs coming from the arrival sequence are met, in order to be sure that a ready job will be eventually scheduled. *) Hypothesis H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched. (** We define [max_dl] as the maximum deadline for all jobs arrived before [t]. *) Let max_dl := max_deadline_for_jobs_arrived_before arr_seq t. (** Next, we define [search_result] as the result of the search for a swap candidate. In order to take the first result, it is sufficient to define the ordering function as a constant false. *) Definition order (_ _ : nat) := false. Definition search_result := search_arg sched (relevant_pstate t) order t max_dl. (** First, we consider the case in which the procedure finds a job to swap with. *) Section MakeWCAtFindsReadyJobs_CaseResultFound. (** Assuming that the processor is idle at time t... *) Hypothesis H_sched_t_idle: is_idle sched t. (** ...let [t_swap] be a time instant found by the search procedure. *) Variable t_swap: instant. Hypothesis search_result_found: search_result = Some t_swap. (** We show that, since the search only yields relevant processor states, a job is found. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
search_result_found: search_result = Some t_swap

exists j : Job, swapped sched t t_swap t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
search_result_found: search_result = Some t_swap

exists j : Job, swapped sched t t_swap t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
search_result_found: relevant_pstate t (sched t_swap)

exists j : Job, swapped sched t t_swap t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
search_result_found: relevant_pstate t (sched t_swap)

match sched t_swap with | Some j => job_arrival j <= t | None => false end -> exists j : Job, swapped sched t t_swap t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)

job_arrival j_swap <= t -> exists j : Job, swapped sched t t_swap t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t

exists j : Job, swapped sched t t_swap t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t

exists j : Job, (if t_swap == t then sched t else if t == t then sched t_swap else sched t) = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SAME_SWAP: (t_swap == t) = true

exists j : Job, sched t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SAME_SWAP: (t_swap == t) = false
exists j : Job, (if t == t then sched t_swap else sched t) = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SAME_SWAP: (t_swap == t) = true

exists j : Job, sched t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SAME_SWAP: (t_swap == t) = false
exists j : Job, (if t == t then sched t_swap else sched t) = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
j_swap: Job
SCHED: sched t = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t

exists j : Job, sched t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SAME_SWAP: (t_swap == t) = false
exists j : Job, (if t == t then sched t_swap else sched t) = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
j_swap: Job
SCHED: sched t = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SCHED_NONE: sched t = None

exists j : Job, sched t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SAME_SWAP: (t_swap == t) = false
exists j : Job, (if t == t then sched t_swap else sched t) = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SAME_SWAP: (t_swap == t) = false

exists j : Job, (if t == t then sched t_swap else sched t) = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SAME_SWAP: (t_swap == t) = false

exists j : Job, (if t == t then sched t_swap else sched t) = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_sched_t_idle: is_idle sched t
t_swap: instant
j_swap: Job
SCHED: sched t_swap = Some j_swap
search_result_found: relevant_pstate t (Some j_swap)
ARR: job_arrival j_swap <= t
SAME_SWAP: (t_swap == t) = false

(if t == t then sched t_swap else sched t) = Some j_swap
by rewrite eq_refl; apply SCHED. Qed. End MakeWCAtFindsReadyJobs_CaseResultFound. (** Conversely, we prove that assuming that the search yields no result brings to a contradiction. *) Section MakeWCAtFindsReadyJobs_CaseResultNone. (** Consider a job that arrives in the arrival sequence, and assume that it is ready at time [t] in the transformed schedule. *) Variable j: Job. Hypothesis H_arrives_in: arrives_in arr_seq j. Hypothesis H_job_ready_sched': job_ready sched' j t. (** Moreover, assume the search for a swap candidate yields nothing. *) Hypothesis H_search_result_none: search_result = None. (** First, note that, since nothing was found, it means there is no relevant processor state between [t] and [max_dl]. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

forall t' : nat, t <= t' < max_dl -> ~~ relevant_pstate t (sched t')
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

forall t' : nat, t <= t' < max_dl -> ~~ relevant_pstate t (sched t')
by apply (search_arg_none _ _ (fun _ _ => false)). Qed. (** Since [j] is ready at time [t], then it must be incomplete. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

service sched j t < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

service sched j t < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
READY_ORIG: job_ready sched j t

service sched j t < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
READY_ORIG: job_ready sched j t

service sched j t < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR_: has_arrived j t
NOT_COMPL_ORIG: ~~ completed_by sched j t

service sched j t < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR_: has_arrived j t
NOT_COMPL_ORIG: ~~ (job_cost j <= service sched j t)

service sched j t < job_cost j
by rewrite leqNgt; apply NOT_COMPL_ORIG. Qed. (** And since [j] is incomplete and meets its deadline, the deadline of [j] is in the future. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

t <= job_deadline j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

t <= job_deadline j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
MEETS_DL_j: job_meets_deadline sched j

t <= job_deadline j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
MEETS_DL_j: job_meets_deadline sched j
LEQ_t1: job_deadline j < t

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
LEQ_t1: job_deadline j < t

service sched j (job_deadline j) < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
LEQ_t1: job_deadline j < t

service sched j (job_deadline j) <= service sched j t
by apply service_monotonic, ltnW. Qed. (** On the other hand, since we know that there is no relevant state between [t] and [max_dl], then it must be the case that [j] is never scheduled in this period, and hence gets no service. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

service sched j t = service sched j max_dl
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

service sched j t = service sched j max_dl
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t

service sched j t = service sched j max_dl
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t

service sched j t = service sched j t + service_during sched j t max_dl
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t

service_during sched j t max_dl = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
ZERO_SERVICE: service_during sched j t max_dl = 0
service sched j t = service sched j t + service_during sched j t max_dl
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t

service_during sched j t max_dl = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t

ideal_progress_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
forall t0 : nat, t <= t0 < max_dl -> ~~ scheduled_at sched j t0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t

forall t0 : nat, t <= t0 < max_dl -> ~~ scheduled_at sched j t0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
t_at: nat
RANGE: t <= t_at < max_dl

~~ scheduled_at sched j t_at
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
t_at: nat
RANGE: t <= t_at < max_dl
NOT_REL: ~~ relevant_pstate t (sched t_at)

~~ scheduled_at sched j t_at
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
t_at: nat
RANGE: t <= t_at < max_dl
NOT_REL: ~~ relevant_pstate t (sched t_at)

sched t_at != Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
t_at: nat
RANGE: t <= t_at < max_dl
NOT_REL: ~~ relevant_pstate t (sched t_at)
EQ: sched t_at = Some j

False
by move: NOT_REL => /negP T; apply: T; rewrite EQ.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
ZERO_SERVICE: service_during sched j t max_dl = 0

service sched j t = service sched j t + service_during sched j t max_dl
by rewrite ZERO_SERVICE; rewrite addn0. Qed. (** Combining the previous lemmas, we can deduce that [j] misses its deadline. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

service sched j (job_deadline j) < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

service sched j (job_deadline j) < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t

service sched j (job_deadline j) < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j t < job_cost j

service sched j (job_deadline j) < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j max_dl < job_cost j

service sched j (job_deadline j) < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
H_all_deadlines_of_arrivals_met: job_meets_deadline sched j
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j max_dl < job_cost j

service sched j (job_deadline j) < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
H_all_deadlines_of_arrivals_met: job_cost j <= service sched j (job_deadline j)
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j max_dl < job_cost j

service sched j (job_deadline j) < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
H_all_deadlines_of_arrivals_met: job_cost j <= service sched j (job_deadline j)
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j max_dl < job_cost j

service sched j (job_deadline j) <= ?n
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
H_all_deadlines_of_arrivals_met: job_cost j <= service sched j (job_deadline j)
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j max_dl < job_cost j
?n < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
H_all_deadlines_of_arrivals_met: job_cost j <= service sched j (job_deadline j)
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j max_dl < job_cost j

service sched j (job_deadline j) <= ?n
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
H_all_deadlines_of_arrivals_met: job_cost j <= service sched j (job_deadline j)
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j max_dl < job_cost j
?n < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
H_all_deadlines_of_arrivals_met: job_cost j <= service sched j (job_deadline j)
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j max_dl < job_cost j

service sched j (max_deadline_for_jobs_arrived_before arr_seq t) < job_cost j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
H_all_deadlines_of_arrivals_met: job_cost j <= service sched j (job_deadline j)
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
ARR: has_arrived j t
NOT_COMPL_sched': ~~ completed_by sched' j t
J_LESS: service sched j max_dl < job_cost j

service sched j (max_deadline_for_jobs_arrived_before arr_seq t) < job_cost j
by apply J_LESS. Qed. (** The fact that [j] misses its deadline contradicts the fact that all deadlines of jobs coming from the arrival sequence are met. We have a contradiction. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
NEQ: job_meets_deadline sched j

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None
NEQ: job_cost j <= service sched j (job_deadline j)

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
j: Job
H_arrives_in: arrives_in arr_seq j
H_job_ready_sched': job_ready sched' j t
H_search_result_none: search_result = None

service sched j (job_deadline j) < job_cost j
by apply j_misses_deadline. Qed. End MakeWCAtFindsReadyJobs_CaseResultNone. (** Next, we show that [make_wc_at] always manages to establish the work-conservation property at the given time. Using the above case analysis, we can conclude that the presence of a ready job always leads to a valid swap. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat

all_deadlines_of_arrivals_met arr_seq sched -> is_work_conserving_at sched' t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat

all_deadlines_of_arrivals_met arr_seq sched -> is_work_conserving_at sched' t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: exists j : Job, arrives_in arr_seq j /\ job_ready sched' j t

exists j : Job, sched' t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: exists j : Job, arrives_in arr_seq j /\ job_ready sched' j t
SCHED_WC_t: sched t = None

exists j : Job, sched' t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
SCHED_WC_t: sched t = None
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t

exists j : Job, sched' t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
SCHED_WC_t: sched t = None
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t

exists j : Job, match sched t with | Some _ => sched | None => swapped sched t (find_swap_candidate arr_seq sched t) end t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
SCHED_WC_t: sched t = None
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t

exists j : Job, swapped sched t match search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) with | Some t_swap => t_swap | None => t end t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
SCHED_WC_t: sched t = None
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t
t_swap: nat
SEARCH_RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = Some t_swap

exists j : Job, swapped sched t t_swap t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
SCHED_WC_t: sched t = None
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t
SEARCH_RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = None
exists j : Job, swapped sched t t t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
SCHED_WC_t: sched t = None
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t
t_swap: nat
SEARCH_RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = Some t_swap

exists j : Job, swapped sched t t_swap t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
SCHED_WC_t: sched t = None
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t
SEARCH_RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = None
exists j : Job, swapped sched t t t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
SCHED_WC_t: sched t = None
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t
SEARCH_RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = None

exists j : Job, swapped sched t t t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
max_dl:= max_deadline_for_jobs_arrived_before arr_seq t: nat
ALL_DL_MET: all_deadlines_of_arrivals_met arr_seq sched
SCHED_WC_t: sched t = None
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t
SEARCH_RES: search_arg sched (relevant_pstate t) (fun=> xpred0) t (max_deadline_for_jobs_arrived_before arr_seq t) = None

exists j : Job, swapped sched t t t = Some j
by exfalso; apply (make_wc_at_case_result_none j); eauto. Qed. End MakeWCAtFindsReadyJobs. (** Next we prove that, given a schedule that respects the work-conservation property until [t-1], applying the point-wise transformation at time [t] will extend the property until [t]. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

all_deadlines_of_arrivals_met arr_seq sched -> (forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l) -> forall t_l : nat, t_l <= t -> is_work_conserving_at sched' t_l
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

all_deadlines_of_arrivals_met arr_seq sched -> (forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l) -> forall t_l : nat, t_l <= t -> is_work_conserving_at sched' t_l
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'

exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat

exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc

exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t

exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tGE: t <= t'
exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t

exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t

sched' t' = sched t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t
SAME: sched' t' = sched t'
exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t

sched' t' = sched t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t

match sched t with | Some _ => sched | None => swapped sched t (find_swap_candidate arr_seq sched t) end t' = sched t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t

swapped sched t (find_swap_candidate arr_seq sched t) t' = sched t'
by rewrite (swap_before_invariant sched t fsc) //.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t
SAME: sched' t' = sched t'

exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t
SAME: sched' t' = sched t'

exists j : Job, sched t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t
SAME: sched' t' = sched t'

exists j : Job, arrives_in arr_seq j /\ job_ready sched j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tLT: t' < t
SAME: sched' t' = sched t'

job_ready sched j t'
by eapply mwa_ready_job_also_ready_in_original_schedule, READY.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tGE: t <= t'

exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tGE: t <= t'

exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tGE: t <= t'

t' = t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tGE: t <= t'
EQ: t' = t
exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tGE: t <= t'

t' = t
by apply /eqP; rewrite eqn_leq; apply /andP; split.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
t': nat
T_MIN: t' <= t
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t'
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc
tGE: t <= t'
EQ: t' = t

exists j : Job, sched' t' = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc

exists j : Job, sched' t = Some j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
PROP: all_deadlines_of_arrivals_met arr_seq sched
P_PREFIX: forall t_l : nat, t_l < t -> is_work_conserving_at sched t_l
j: Job
ARR_IN: arrives_in arr_seq j
READY: job_ready sched' j t
fsc:= find_swap_candidate arr_seq sched t: nat
LEQ_fsc: t <= fsc

exists j : Job, arrives_in arr_seq j /\ job_ready sched' j t
by exists j; split; eauto. } Qed. (** We now show that the point-wise transformation does not introduce any new job that does not come from the arrival sequence. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

jobs_come_from_arrival_sequence sched arr_seq -> jobs_come_from_arrival_sequence sched' arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

jobs_come_from_arrival_sequence sched arr_seq -> jobs_come_from_arrival_sequence sched' arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

jobs_come_from_arrival_sequence sched arr_seq -> jobs_come_from_arrival_sequence match sched t with | Some _ => sched | None => swapped sched t (find_swap_candidate arr_seq sched t) end arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
SCHED_orig: sched t = None

jobs_come_from_arrival_sequence sched arr_seq -> jobs_come_from_arrival_sequence (swapped sched t (find_swap_candidate arr_seq sched t)) arr_seq
by apply swapped_jobs_come_from_arrival_sequence. Qed. (** We also show that the point-wise transformation does not schedule jobs in instants in which they are not ready. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

jobs_must_be_ready_to_execute sched -> jobs_must_be_ready_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

jobs_must_be_ready_to_execute sched -> jobs_must_be_ready_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
READY: jobs_must_be_ready_to_execute sched

jobs_must_be_ready_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
READY: jobs_must_be_ready_to_execute sched

jobs_must_be_ready_to_execute match sched t with | Some _ => sched | None => swapped sched t (find_swap_candidate arr_seq sched t) end
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
READY: jobs_must_be_ready_to_execute sched
SCHED_orig: sched t = None

jobs_must_be_ready_to_execute (swapped sched t (find_swap_candidate arr_seq sched t))
by apply fsc_jobs_must_be_ready_to_execute. Qed. (** Finally, we show that the point-wise transformation does not introduce deadline misses. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

all_deadlines_of_arrivals_met arr_seq sched -> all_deadlines_of_arrivals_met arr_seq sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)

all_deadlines_of_arrivals_met arr_seq sched -> all_deadlines_of_arrivals_met arr_seq sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
ALL: all_deadlines_of_arrivals_met arr_seq sched
j: Job
ARR: arrives_in arr_seq j

job_meets_deadline sched' j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
ALL: job_meets_deadline sched j
ARR: arrives_in arr_seq j

job_meets_deadline sched' j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
t: instant
sched':= make_wc_at arr_seq sched t: schedule (processor_state Job)
j: Job
ALL: job_cost j <= service sched j (job_deadline j)
ARR: arrives_in arr_seq j

job_cost j <= service sched' j (job_deadline j)
by apply (leq_trans ALL (mwa_service_bound _ _)). Qed. End MakeWCAtFacts. (** In the following section, we proceed by proving some useful properties respected by the partial schedule obtained by applying the work-conservation transformation up to an arbitrary horizon. *) Section PrefixFacts. (** Consider an ideal uniprocessor schedule. *) Variable sched: schedule (ideal.processor_state Job). (** We start by proving that the transformation performed with two different horizons will yield two schedules that are identical until the earlier horizon. *) Section PrefixInclusion. (** Consider two horizons... *) Variable h1 h2: instant. (** ...and assume w.l.o.g. that they are ordered... *) Hypothesis H_horizon_order: h1 <= h2. (** ...we define two schedules, resulting from the transformation performed, respectively, until the first and the second horizon. *) Let sched1 := wc_transform_prefix arr_seq sched h1. Let sched2 := wc_transform_prefix arr_seq sched h2. (** Then, we show that the two schedules are guaranteed to be equal until the earlier horizon. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
H_horizon_order: h1 <= h2
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched h2: schedule (processor_state Job)

forall t : nat, t < h1 -> sched1 t = sched2 t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
H_horizon_order: h1 <= h2
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched h2: schedule (processor_state Job)

forall t : nat, t < h1 -> sched1 t = sched2 t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
H_horizon_order: h1 <= h2
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched h2: schedule (processor_state Job)
t: nat
before_horizon: t < h1

sched1 t = sched2 t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
H_horizon_order: h1 <= h2
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched h2: schedule (processor_state Job)
t: nat
before_horizon: t < h1

wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched h2 t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t

wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i.+1 t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t

h1 <= i.+1 -> wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i.+1 t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t
LT: h1 < i.+1

wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i.+1 t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t

h1 < i.+1 -> wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i.+1 t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t
H_horizon_order_lt: h1 <= i

wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i.+1 t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t
H_horizon_order_lt: h1 <= i

wc_transform_prefix arr_seq sched i t = make_wc_at arr_seq (prefix_map sched (make_wc_at arr_seq) i) i t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t
H_horizon_order_lt: h1 <= i

wc_transform_prefix arr_seq sched i t = match prefix_map sched (make_wc_at arr_seq) i i with | Some _ => prefix_map sched (make_wc_at arr_seq) i | None => swapped (prefix_map sched (make_wc_at arr_seq) i) i (find_swap_candidate arr_seq (prefix_map sched (make_wc_at arr_seq) i) i) end t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t
H_horizon_order_lt: h1 <= i
SCHED: prefix_map sched (make_wc_at arr_seq) i i = None

wc_transform_prefix arr_seq sched i t = swapped (prefix_map sched (make_wc_at arr_seq) i) i (find_swap_candidate arr_seq (prefix_map sched (make_wc_at arr_seq) i) i) t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t
H_horizon_order_lt: h1 <= i
SCHED: prefix_map sched (make_wc_at arr_seq) i i = None

wc_transform_prefix arr_seq sched i t = prefix_map sched (make_wc_at arr_seq) i t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t
H_horizon_order_lt: h1 <= i
SCHED: prefix_map sched (make_wc_at arr_seq) i i = None
i <= find_swap_candidate arr_seq (wc_transform_prefix arr_seq sched i) i
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h1, h2: instant
i: nat
H_horizon_order: h1 <= i.+1
sched1:= wc_transform_prefix arr_seq sched h1: schedule (processor_state Job)
sched2:= wc_transform_prefix arr_seq sched i.+1: schedule (processor_state Job)
t: nat
before_horizon: t < h1
IHi: h1 <= i -> let sched2 := wc_transform_prefix arr_seq sched i in wc_transform_prefix arr_seq sched h1 t = wc_transform_prefix arr_seq sched i t
H_horizon_order_lt: h1 <= i
SCHED: prefix_map sched (make_wc_at arr_seq) i i = None

i <= find_swap_candidate arr_seq (wc_transform_prefix arr_seq sched i) i
apply swap_candidate_is_in_future. Qed. End PrefixInclusion. (** Next, we show that repeating the point-wise transformation up to a given horizon does not introduce any deadline miss. *) Section JobsMeetDeadlinePrefix. (** Assuming that all deadlines of jobs coming from the arrival sequence are met... *) Hypothesis H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched. (** ...let us define [sched'] as the schedule resulting from the full work-conservation transformation. Note that, if the schedule is sampled at time [t], the transformation is performed until [t+1]. *) Let sched' := wc_transform arr_seq sched. (** Consider a job from the arrival sequence. *) Variable j: Job. Hypothesis H_arrives_in: arrives_in arr_seq j. (** We show that, in the transformed schedule, the service of the job is always greater or equal than in the original one, at any given time. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j

forall t : instant, service sched j t <= service sched' j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j

forall t : instant, service sched j t <= service sched' j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant

service sched j t <= service sched' j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant

service sched j t <= service (fun t : nat => wc_transform_prefix arr_seq sched t.+1 t) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat

service sched j t <= serv
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat

service sched j t <= serv
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat

serv = servp
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat
service sched j t <= servp
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat

serv = servp
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat

\sum_(0 <= t < t) service_at (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t = \sum_(0 <= t0 < t) service_at (wc_transform_prefix arr_seq sched t.+1) j t0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat
t': nat
LT_t: t' < t

service_at (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t' = service_at (wc_transform_prefix arr_seq sched t.+1) j t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat
t': nat
LT_t: t' < t

service_in j (wc_transform_prefix arr_seq sched t'.+1 t') = service_in j (wc_transform_prefix arr_seq sched t.+1 t')
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat
t': nat
LT_t: t' < t

t' < t.+1
by auto.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat

service sched j t <= servp
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
serv:= service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t: nat
servp:= service (wc_transform_prefix arr_seq sched t.+1) j t: nat

service sched j t <= service (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant

service sched j t <= service (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant

forall (sched0 : schedule (processor_state Job)) (t0 : instant), service sched j t <= service sched0 j t -> service sched j t <= service (make_wc_at arr_seq sched0 t0) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
sched0: schedule (processor_state Job)
t0: instant
H2: service sched j t <= service sched0 j t

service sched j t <= service (make_wc_at arr_seq sched0 t0) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j
t: instant
sched0: schedule (processor_state Job)
t0: instant
H2: service sched j t <= service sched0 j t

service sched0 j t <= service (make_wc_at arr_seq sched0 t0) j t
by intros; apply mwa_service_bound. Qed. (** Finally, it follows directly that the transformed schedule cannot introduce a deadline miss for any job from the arrival sequence. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j

job_meets_deadline sched' j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j

job_meets_deadline sched' j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j

job_cost j <= service (wc_transform arr_seq sched) j (job_deadline j)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched':= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
H_arrives_in: arrives_in arr_seq j

job_cost j <= service sched j (job_deadline j)
by apply H_all_deadlines_of_arrivals_met. Qed. End JobsMeetDeadlinePrefix. (** Next, consider a given time, used as horizon for the transformation... *) Variable h: instant. (** ...and let us call [sched'] the schedule resulting from the transformation performed until [h]. *) Let sched' := wc_transform_prefix arr_seq sched h. (** We prove that [sched'] will never introduce jobs not coming from the arrival sequence. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)

jobs_come_from_arrival_sequence sched arr_seq -> jobs_come_from_arrival_sequence sched' arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)

jobs_come_from_arrival_sequence sched arr_seq -> jobs_come_from_arrival_sequence sched' arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)
FROM_ARR: jobs_come_from_arrival_sequence sched arr_seq

jobs_come_from_arrival_sequence sched' arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)
FROM_ARR: jobs_come_from_arrival_sequence sched arr_seq

jobs_come_from_arrival_sequence (prefix_map sched (make_wc_at arr_seq) h) arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)
FROM_ARR: jobs_come_from_arrival_sequence sched arr_seq

forall (sched : schedule (processor_state Job)) (t : instant), jobs_come_from_arrival_sequence sched arr_seq -> jobs_come_from_arrival_sequence (make_wc_at arr_seq sched t) arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)
FROM_ARR: jobs_come_from_arrival_sequence sched arr_seq
schedX: schedule (processor_state Job)
t: instant
ARR: jobs_come_from_arrival_sequence schedX arr_seq

jobs_come_from_arrival_sequence (make_wc_at arr_seq schedX t) arr_seq
by apply mwa_jobs_come_from_arrival_sequence. Qed. (** Similarly, we can show that [sched'] will only schedule jobs if they are ready. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)

jobs_must_be_ready_to_execute sched -> jobs_must_be_ready_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)

jobs_must_be_ready_to_execute sched -> jobs_must_be_ready_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)
READY: jobs_must_be_ready_to_execute sched

jobs_must_be_ready_to_execute sched'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)
READY: jobs_must_be_ready_to_execute sched

jobs_must_be_ready_to_execute (prefix_map sched (make_wc_at arr_seq) h)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)
READY: jobs_must_be_ready_to_execute sched

forall (sched : schedule (processor_state Job)) (t : instant), jobs_must_be_ready_to_execute sched -> jobs_must_be_ready_to_execute (make_wc_at arr_seq sched t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
h: instant
sched':= wc_transform_prefix arr_seq sched h: schedule (processor_state Job)
READY: jobs_must_be_ready_to_execute sched
schedX: schedule (processor_state Job)
t: instant
ARR: jobs_must_be_ready_to_execute schedX

jobs_must_be_ready_to_execute (make_wc_at arr_seq schedX t)
by apply mwa_jobs_must_be_ready_to_execute. Qed. End PrefixFacts. End AuxiliaryLemmasWorkConservingTransformation. (** Finally, we can leverage all the previous results to prove statements about the full work-conservation transformation. *) Section WorkConservingTransformation. (** 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, costs, and deadlines... *) Context {Job : JobType}. Context `{JobArrival Job}. Context `{JobCost Job}. Context `{JobDeadline Job}. (** ...an arbitrary valid arrival sequence... *) Variable arr_seq: arrival_sequence Job. Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq. (** ...and an ideal uniprocessor schedule... *) Variable sched: schedule (ideal.processor_state Job). (** ...in which jobs come from the arrival sequence, and must be ready to execute... *) Hypothesis H_sched_valid: valid_schedule sched arr_seq. (** ...and in which no job misses a deadline. *) Hypothesis H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched. (** Let us call [sched_wc] the schedule obtained after applying the work-conservation transformation. *) Let sched_wc := wc_transform arr_seq sched. (** First, we show that any scheduled job still comes from the arrival sequence. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

jobs_come_from_arrival_sequence sched_wc arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

jobs_come_from_arrival_sequence sched_wc arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant

scheduled_at sched_wc j t -> arrives_in arr_seq j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant

scheduled_at sched_wc j t -> arrives_in arr_seq j
eapply (wc_prefix_jobs_come_from_arrival_sequence arr_seq sched t.+1); rt_eauto. Qed. (** Similarly, jobs are only scheduled if they are ready. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

jobs_must_be_ready_to_execute sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

jobs_must_be_ready_to_execute sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant

scheduled_at sched_wc j t -> job_ready sched_wc j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
SCHED_AT: scheduled_at (wc_transform_prefix arr_seq sched t.+1) j t

job_ready (fun t : nat => wc_transform_prefix arr_seq sched t.+1 t) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
SCHED_AT: scheduled_at (wc_transform_prefix arr_seq sched t.+1) j t
READY': job_ready (wc_transform_prefix arr_seq sched t.+1) j t

job_ready (fun t : nat => wc_transform_prefix arr_seq sched t.+1 t) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
SCHED_AT: scheduled_at (wc_transform_prefix arr_seq sched t.+1) j t

job_ready (wc_transform_prefix arr_seq sched t.+1) j t -> job_ready (fun t : nat => wc_transform_prefix arr_seq sched t.+1 t) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
SCHED_AT: scheduled_at (wc_transform_prefix arr_seq sched t.+1) j t

has_arrived j t && ~~ (job_cost j <= service_during (wc_transform_prefix arr_seq sched t.+1) j 0 t) -> has_arrived j t && ~~ (job_cost j <= service_during (fun t : nat => wc_transform_prefix arr_seq sched t.+1 t) j 0 t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
SCHED_AT: scheduled_at (wc_transform_prefix arr_seq sched t.+1) j t

forall t0 : nat, 0 <= t0 < t -> sched_wc t0 = wc_transform_prefix arr_seq sched t.+1 t0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
SCHED_AT: scheduled_at (wc_transform_prefix arr_seq sched t.+1) j t
t': nat
BOUND_t': t' < t

sched_wc t' = wc_transform_prefix arr_seq sched t.+1 t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
SCHED_AT: scheduled_at (wc_transform_prefix arr_seq sched t.+1) j t
t': nat
BOUND_t': t' < t

wc_transform_prefix arr_seq sched t'.+1 t' = wc_transform_prefix arr_seq sched t.+1 t'
by apply wc_transform_prefix_inclusion => //; rewrite ltnS; apply ltnW. Qed. (** Also, no deadline misses are introduced. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

all_deadlines_of_arrivals_met arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

all_deadlines_of_arrivals_met arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
ARR_IN: arrives_in arr_seq j

job_meets_deadline sched_wc j
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
ARR_IN: arrives_in arr_seq j

job_meets_deadline (wc_transform arr_seq sched) j
by apply wc_prefix_job_meets_deadline. Qed. (** Finally, we can show that the transformation leads to a schedule in which the processor is not idle if a job is ready. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

forall (j : Job) (t : instant), job_ready sched_wc j t -> arrives_in arr_seq j -> exists j' : Job, sched_wc t = Some j'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

forall (j : Job) (t : instant), job_ready sched_wc j t -> arrives_in arr_seq j -> exists j' : Job, sched_wc t = Some j'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

exists j' : Job, sched_wc t = Some j'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

exists j' : Job, prefix_map sched (make_wc_at arr_seq) t.+1 t = Some j'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

forall (sched : schedule (processor_state Job)) (t_ref : instant), all_deadlines_of_arrivals_met arr_seq sched -> all_deadlines_of_arrivals_met arr_seq (make_wc_at arr_seq sched t_ref)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
forall (sched : schedule (processor_state Job)) (t_ref : nat), all_deadlines_of_arrivals_met arr_seq sched -> (forall t' : nat, t' < t_ref -> is_work_conserving_at arr_seq sched t') -> forall t' : nat, t' <= t_ref -> is_work_conserving_at arr_seq (make_wc_at arr_seq sched t_ref) t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
exists j : Job, arrives_in arr_seq j /\ job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

forall (sched : schedule (processor_state Job)) (t_ref : instant), all_deadlines_of_arrivals_met arr_seq sched -> all_deadlines_of_arrivals_met arr_seq (make_wc_at arr_seq sched t_ref)
by apply mwa_all_deadlines_of_arrivals_met.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

forall (sched : schedule (processor_state Job)) (t_ref : nat), all_deadlines_of_arrivals_met arr_seq sched -> (forall t' : nat, t' < t_ref -> is_work_conserving_at arr_seq sched t') -> forall t' : nat, t' <= t_ref -> is_work_conserving_at arr_seq (make_wc_at arr_seq sched t_ref) t'
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
exists j : Job, arrives_in arr_seq j /\ job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

forall (sched : schedule (processor_state Job)) (t_ref : nat), all_deadlines_of_arrivals_met arr_seq sched -> (forall t' : nat, t' < t_ref -> is_work_conserving_at arr_seq sched t') -> forall t' : nat, t' <= t_ref -> is_work_conserving_at arr_seq (make_wc_at arr_seq sched t_ref) t'
by intros; apply mwa_establishes_wc.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

exists j : Job, arrives_in arr_seq j /\ job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

exists j : Job, arrives_in arr_seq j /\ job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

arrives_in arr_seq j /\ job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

job_ready sched_wc j t = job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
EQ: job_ready sched_wc j t = job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

job_ready sched_wc j t = job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

has_arrived j t && ~~ (job_cost j <= \sum_(0 <= t < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t)) = has_arrived j t && ~~ (job_cost j <= \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t0))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

true && ~~ (job_cost j <= \sum_(0 <= t < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t)) = true && ~~ (job_cost j <= \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t0))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

\sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t0.+1 t0) = \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t0)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
EQ_SUM: \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t0.+1 t0) = \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t0)
true && ~~ (job_cost j <= \sum_(0 <= t < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t)) = true && ~~ (job_cost j <= \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t0))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j

\sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t0.+1 t0) = \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t0)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
t': nat
LT_t: t' < t

service_in j (prefix_map sched (make_wc_at arr_seq) t'.+1 t') = service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t')
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
t': nat
LT_t: t' < t

service_in j (wc_transform_prefix arr_seq sched t'.+1 t') = service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t')
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
t': nat
LT_t: t' < t

service_in j (wc_transform_prefix arr_seq sched t'.+1 t') = service_in j (wc_transform_prefix arr_seq sched t.+1 t')
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
t': nat
LT_t: t' < t

t' < t.+1
by auto.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
EQ_SUM: \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t0.+1 t0) = \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t0)

true && ~~ (job_cost j <= \sum_(0 <= t < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t)) = true && ~~ (job_cost j <= \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) t.+1 t0))
by rewrite EQ_SUM.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
READY: job_ready sched_wc j t
ARR_IN: arrives_in arr_seq j
EQ: job_ready sched_wc j t = job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t

job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
ARR_IN: arrives_in arr_seq j
EQ: job_ready sched_wc j t = job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t

job_ready sched_wc j t -> job_ready (prefix_map sched (make_wc_at arr_seq) t.+1) j t
by rewrite EQ. } Qed. (** We can easily extend the previous lemma to obtain the definition of a work-conserving schedule. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
ARR_IN: arrives_in arr_seq j

backlogged sched_wc j t -> exists j_other : Job, scheduled_at sched_wc j_other t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
ARR_IN: arrives_in arr_seq j
READY: job_ready sched_wc j t

exists j_other : Job, scheduled_at sched_wc j_other t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
j: Job
t: instant
ARR_IN: arrives_in arr_seq j
READY: job_ready sched_wc j t
j': Job
SCHED_wc: sched_wc t = Some j'

exists j_other : Job, scheduled_at sched_wc j_other t
by exists j'; rewrite scheduled_at_def; apply /eqP. Qed. (** Ultimately, we can show that the work-conservation transformation maintains all the properties of validity, does not introduce new deadline misses, and establishes the work-conservation property. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

valid_schedule sched_wc arr_seq /\ all_deadlines_of_arrivals_met arr_seq sched_wc /\ work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

valid_schedule sched_wc arr_seq /\ all_deadlines_of_arrivals_met arr_seq sched_wc /\ work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

jobs_come_from_arrival_sequence sched_wc arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
jobs_must_be_ready_to_execute sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
all_deadlines_of_arrivals_met arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

jobs_come_from_arrival_sequence sched_wc arr_seq
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
jobs_must_be_ready_to_execute sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
all_deadlines_of_arrivals_met arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

jobs_must_be_ready_to_execute sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
all_deadlines_of_arrivals_met arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

jobs_must_be_ready_to_execute sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
all_deadlines_of_arrivals_met arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

all_deadlines_of_arrivals_met arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

all_deadlines_of_arrivals_met arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job
work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

work_conserving arr_seq sched_wc
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_all_deadlines_of_arrivals_met: all_deadlines_of_arrivals_met arr_seq sched
sched_wc:= wc_transform arr_seq sched: nat -> processor_state Job

work_conserving arr_seq sched_wc
apply wc_is_work_conserving. Qed. End WorkConservingTransformation.