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]
(** * Arrival Sequence *) (** First, we relate the stronger to the weaker arrival predicates. *) Section ArrivalPredicates. (** Consider any kinds of jobs with arrival times. *) Context {Job : JobType} `{JobArrival Job}. (** A job that arrives in some interval <<[t1, t2)>> certainly arrives before time [t2]. *)
Job: JobType
H: JobArrival Job

forall (j : Job) (t1 t2 : instant), arrived_between j t1 t2 -> arrived_before j t2
Job: JobType
H: JobArrival Job

forall (j : Job) (t1 t2 : instant), arrived_between j t1 t2 -> arrived_before j t2
by move=> ? ? ? /andP[]. Qed. (** A job that arrives before a time [t] certainly has arrived by time [t]. *)
Job: JobType
H: JobArrival Job

forall (j : Job) (t : instant), arrived_before j t -> has_arrived j t
Job: JobType
H: JobArrival Job

forall (j : Job) (t : instant), arrived_before j t -> has_arrived j t
move=> ? ?; exact: ltnW. Qed. (** Furthermore, we restate a common hypothesis to make its implication easier to discover. *)
Job: JobType
H: JobArrival Job

forall arr_seq : arrival_sequence Job, valid_arrival_sequence arr_seq -> consistent_arrival_times arr_seq
Job: JobType
H: JobArrival Job

forall arr_seq : arrival_sequence Job, valid_arrival_sequence arr_seq -> consistent_arrival_times arr_seq
by move=> ? []. Qed. (** We restate another common hypothesis to make its implication easier to discover. *)
Job: JobType
H: JobArrival Job

forall arr_seq : arrival_sequence Job, valid_arrival_sequence arr_seq -> arrival_sequence_uniq arr_seq
Job: JobType
H: JobArrival Job

forall arr_seq : arrival_sequence Job, valid_arrival_sequence arr_seq -> arrival_sequence_uniq arr_seq
by move=> ? []. Qed. End ArrivalPredicates. (** In this section, we relate job readiness to [has_arrived]. *) Section Arrived. (** Consider any kinds of jobs and any kind of processor state. *) Context {Job : JobType} {PState : ProcessorState Job}. (** Consider any schedule... *) Variable sched : schedule PState. (** ...and suppose that jobs have a cost, an arrival time, and a notion of readiness. *) Context `{JobCost Job}. Context `{JobArrival Job}. Context {jr : JobReady Job PState}. (** First, we note that readiness models are by definition consistent w.r.t. [pending]. *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), job_ready sched j t -> pending sched j t
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), job_ready sched j t -> pending sched j t
move: jr => [? +] /= ?; exact. Qed. (** Next, we observe that a given job must have arrived to be ready... *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), job_ready sched j t -> has_arrived j t
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), job_ready sched j t -> has_arrived j t
by move=> ? ? /any_ready_job_is_pending => /andP[]. Qed. (** ...and lift this observation also to the level of whole schedules. *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

jobs_must_be_ready_to_execute sched -> jobs_must_arrive_to_execute sched
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

jobs_must_be_ready_to_execute sched -> jobs_must_arrive_to_execute sched
move=> READY ? ? ?; exact/ready_implies_arrived/READY. Qed. (** Furthermore, in a valid schedule, jobs must arrive to execute. *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall arr_seq : arrival_sequence Job, valid_schedule sched arr_seq -> jobs_must_arrive_to_execute sched
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall arr_seq : arrival_sequence Job, valid_schedule sched arr_seq -> jobs_must_arrive_to_execute sched
move=> ? [? ?]; exact: jobs_must_arrive_to_be_ready. Qed. (** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), backlogged sched j t -> has_arrived j t
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), backlogged sched j t -> has_arrived j t
move=> ? ? /andP[? ?]; exact: ready_implies_arrived. Qed. (** Similarly, since backlogged jobs are by definition pending, any backlogged job must be incomplete. *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), backlogged sched j t -> ~~ completed_by sched j t
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), backlogged sched j t -> ~~ completed_by sched j t
by move=> ? ? /andP[/any_ready_job_is_pending /andP[]]. Qed. (** Finally, we restate common hypotheses on the well-formedness of schedules to make their implications more easily discoverable. First, on the readiness of scheduled jobs, ... *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

jobs_must_be_ready_to_execute sched -> forall (j : Job) (t : instant), scheduled_at sched j t -> job_ready sched j t
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

jobs_must_be_ready_to_execute sched -> forall (j : Job) (t : instant), scheduled_at sched j t -> job_ready sched j t
exact. Qed. (** ... second, on the origin of scheduled jobs, and ... *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall arr_seq : arrival_sequence Job, valid_schedule sched arr_seq -> jobs_come_from_arrival_sequence sched arr_seq
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall arr_seq : arrival_sequence Job, valid_schedule sched arr_seq -> jobs_come_from_arrival_sequence sched arr_seq
by move=> ? []. Qed. (** ... third, on the readiness of jobs in valid schedules. *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall arr_seq : arrival_sequence Job, valid_schedule sched arr_seq -> jobs_must_be_ready_to_execute sched
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall arr_seq : arrival_sequence Job, valid_schedule sched arr_seq -> jobs_must_be_ready_to_execute sched
by move=> ? []. Qed. End Arrived. (** In this section, we establish useful facts about arrival sequence prefixes. *) Section ArrivalSequencePrefix. (** Consider any kind of tasks and jobs. *) Context {Job: JobType}. Context {Task : TaskType}. Context `{JobArrival Job}. Context `{JobTask Job Task}. (** Consider any job arrival sequence. *) Variable arr_seq: arrival_sequence Job. (** We begin with basic lemmas for manipulating the sequences. *) Section Composition. (** We show that the set of arriving jobs can be split into disjoint intervals. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job

forall t1 t t2 : nat, t1 <= t -> t <= t2 -> arrivals_between arr_seq t1 t2 = arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job

forall t1 t t2 : nat, t1 <= t -> t <= t2 -> arrivals_between arr_seq t1 t2 = arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2
by move=> ? ? ? ? ?; rewrite -big_cat_nat. Qed. (** We also prove a stronger version of the above lemma in the case of arrivals that satisfy a predicate [P]. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job

forall (P : Job -> bool) (t t1 t2 : nat), t1 <= t < t2 -> arrivals_between_P arr_seq P t1 t2 = arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job

forall (P : Job -> bool) (t t1 t2 : nat), t1 <= t < t2 -> arrivals_between_P arr_seq P t1 t2 = arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
P: Job -> bool
t, t1, t2: nat

t1 <= t < t2 -> arrivals_between_P arr_seq P t1 t2 = arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2
by move=> /andP[? ?]; rewrite -filter_cat -arrivals_between_cat// ltnW. Qed. (** The same observation applies to membership in the set of arrived jobs. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job

forall (j : Job) (t1 t t2 : nat), t1 <= t -> t <= t2 -> (j \in arrivals_between arr_seq t1 t2) = (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job

forall (j : Job) (t1 t t2 : nat), t1 <= t -> t <= t2 -> (j \in arrivals_between arr_seq t1 t2) = (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2)
by move=> ? ? ? ? ? ?; rewrite -arrivals_between_cat. Qed. (** We observe that we can grow the considered interval without "losing" any arrived jobs, i.e., membership in the set of arrived jobs is monotonic. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job

forall (j : Job) (t1 t1' t2 t2' : nat), t1' <= t1 -> t2 <= t2' -> j \in arrivals_between arr_seq t1 t2 -> j \in arrivals_between arr_seq t1' t2'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job

forall (j : Job) (t1 t1' t2 t2' : nat), t1' <= t1 -> t2 <= t2' -> j \in arrivals_between arr_seq t1 t2 -> j \in arrivals_between arr_seq t1' t2'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2

j \in arrivals_between arr_seq t1' t2'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t2_le_t1: t2 <= t1

j \in arrivals_between arr_seq t1' t2'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2
j \in arrivals_between arr_seq t1' t2'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t2_le_t1: t2 <= t1

j \in arrivals_between arr_seq t1' t2'
by move: j_in; rewrite /arrivals_between big_geq.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2

j \in arrivals_between arr_seq t1' t2'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2

(j \in arrivals_between arr_seq t1' t1) || (j \in arrivals_between arr_seq t1 t2')
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2
t1 <= t2'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2

t1 <= t2'
exact: leq_trans t2_le_t2'.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2

(j \in arrivals_between arr_seq t1' t1) || (j \in arrivals_between arr_seq t1 t2')
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2

[|| j \in arrivals_between arr_seq t1' t1, j \in arrivals_between arr_seq t1 t2 | j \in arrivals_between arr_seq t2 t2']
by rewrite j_in orbT. Qed. End Composition. (** Next, we relate the arrival prefixes with job arrival times. *) Section ArrivalTimes. (** Assume that job arrival times are consistent. *) Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq. (** To make the hypothesis and its implication easier to discover, we restate it as a trivial lemma. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t : instant), arrives_at arr_seq j t -> job_arrival j = t
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t : instant), arrives_at arr_seq j t -> job_arrival j = t
exact: H_consistent_arrival_times. Qed. (** Similarly, to simplify subsequent proofs, we restate the [H_consistent_arrival_times] assumption as a trivial corollary. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t : instant), j \in arrivals_at arr_seq t -> job_arrival j = t
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t : instant), j \in arrivals_at arr_seq t -> job_arrival j = t
exact: H_consistent_arrival_times. Qed. (** To begin with actual properties, we observe that any job in the set of all arrivals between time instants [t1] and [t2] must arrive in the interval <<[t1,t2)>>. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j < t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j < t2
by move=> ? ? ? /mem_bigcat_nat_exists[i [/job_arrival_at <-]]. Qed. (** For convenience, we restate the left bound of the above lemma... *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j
by move=> ? ? ? /job_arrival_between/andP[]. Qed. (** ... as well as the right bound separately as corollaries. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> job_arrival j < t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> job_arrival j < t2
by move=> ? ? ? /job_arrival_between/andP[]. Qed. (** Second, we prove that if a job belongs to the prefix (jobs_arrived_before t), then it arrives in the arrival sequence. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> arrives_in arr_seq j
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> arrives_in arr_seq j
by move=> ? ? ? /mem_bigcat_nat_exists[arr [? _]]; exists arr. Qed. (** We also prove a weaker version of the above lemma. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (t : instant) (j : Job), j \in arr_seq t -> arrives_in arr_seq j
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (t : instant) (j : Job), j \in arr_seq t -> arrives_in arr_seq j
by move=> t ? ?; exists t. Qed. (** Next, we prove that if a job belongs to the prefix (jobs_arrived_between t1 t2), then it indeed arrives between t1 and t2. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> arrived_between j t1 t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), j \in arrivals_between arr_seq t1 t2 -> arrived_between j t1 t2
by move=> ? ? ? /mem_bigcat_nat_exists[t0 [/job_arrival_at <-]]. Qed. (** Similarly, if a job belongs to the prefix (jobs_arrived_before t), then it indeed arrives before time t. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t : instant), j \in arrivals_before arr_seq t -> arrived_before j t
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t : instant), j \in arrivals_before arr_seq t -> arrived_before j t
by move=> ? ? /in_arrivals_implies_arrived_between. Qed. (** Similarly, we prove that if a job from the arrival sequence arrives before t, then it belongs to the sequence (jobs_arrived_before t). *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), arrives_in arr_seq j -> arrived_between j t1 t2 -> j \in arrivals_between arr_seq t1 t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : instant), arrives_in arr_seq j -> arrived_between j t1 t2 -> j \in arrivals_between arr_seq t1 t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j: Job
t1, t2, a_j: instant
arrj: j \in arrivals_at arr_seq a_j
before: arrived_between j t1 t2

t1 <= a_j < t2
by rewrite -(job_arrival_at arrj). Qed. (** Any job in arrivals between time instants [t1] and [t2] must arrive in the interval <<[t1,t2)>>. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (P : Job -> bool) (t1 t2 : instant), j \in arrivals_between_P arr_seq P t1 t2 -> t1 <= job_arrival j < t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (P : Job -> bool) (t1 t2 : instant), j \in arrivals_between_P arr_seq P t1 t2 -> t1 <= job_arrival j < t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j: Job
P: Job -> bool
t1, t2: instant

j \in arrivals_between_P arr_seq P t1 t2 -> t1 <= job_arrival j < t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j: Job
P: Job -> bool
t1, t2: instant
Pj: P j
i: nat
iitv: t1 <= i < t2

j \in arrivals_at arr_seq i -> t1 <= job_arrival j < t2
by move=> /job_arrival_at ->. Qed. (** Any job [j] is in the sequence [arrivals_between t1 t2] given that [j] arrives in the interval <<[t1,t2)>>. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : nat), arrives_in arr_seq j -> t1 <= job_arrival j < t2 -> j \in arrivals_between arr_seq t1 t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j : Job) (t1 t2 : nat), arrives_in arr_seq j -> t1 <= job_arrival j < t2 -> j \in arrivals_between arr_seq t1 t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j: Job
t1, t2: nat
t: instant
jarr: j \in arrivals_at arr_seq t
jitv: t1 <= job_arrival j < t2

t1 <= t < t2
by rewrite -(job_arrival_at jarr). Qed. (** Next, we prove that if the arrival sequence doesn't contain duplicate jobs, the same applies for any of its prefixes. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

arrival_sequence_uniq arr_seq -> forall t1 t2 : instant, uniq (arrivals_between arr_seq t1 t2)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

arrival_sequence_uniq arr_seq -> forall t1 t2 : instant, uniq (arrivals_between arr_seq t1 t2)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
SET: arrival_sequence_uniq arr_seq
t1, t2: instant
j: Job
t1', t2': nat

j \in arrivals_at arr_seq t1' -> j \in arrivals_at arr_seq t2' -> t1' = t2'
by move=> /job_arrival_at <- /job_arrival_at <-. Qed. (** Also note that there can't by any arrivals in an empty time interval. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall t1 t2 : nat, t2 <= t1 -> arrivals_between arr_seq t1 t2 = [::]
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall t1 t2 : nat, t2 <= t1 -> arrivals_between arr_seq t1 t2 = [::]
by move=> ? ? ?; rewrite /arrivals_between big_geq. Qed. (** Conversely, if a job arrives, the considered interval is non-empty. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (t1 t2 : instant) (j : Job), j \in arrivals_between arr_seq t1 t2 -> t1 < t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (t1 t2 : instant) (j : Job), j \in arrivals_between arr_seq t1 t2 -> t1 < t2
by move=> j1 j2 t; apply: contraPltn=> LEQ; rewrite arrivals_between_geq. Qed. (** Given jobs [j1] and [j2] in [arrivals_between_P arr_seq P t1 t2], the fact that [j2] arrives strictly before [j1] implies that [j2] also belongs in the sequence [arrivals_between_P arr_seq P t1 (job_arrival j1)]. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j1 j2 : Job) (P : Job -> bool) (t1 t2 : instant), j1 \in arrivals_between_P arr_seq P t1 t2 -> j2 \in arrivals_between_P arr_seq P t1 t2 -> job_arrival j2 < job_arrival j1 -> j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall (j1 j2 : Job) (P : Job -> bool) (t1 t2 : instant), j1 \in arrivals_between_P arr_seq P t1 t2 -> j2 \in arrivals_between_P arr_seq P t1 t2 -> job_arrival j2 < job_arrival j1 -> j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant

j1 \in arrivals_between_P arr_seq P t1 t2 -> j2 \in arrivals_between_P arr_seq P t1 t2 -> job_arrival j2 < job_arrival j1 -> j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1

P j2 && (j2 \in arrivals_between arr_seq t1 (job_arrival j1))
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1

arrives_in arr_seq j2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1
t1 <= job_arrival j2 < job_arrival j1
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1

arrives_in arr_seq j2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1
t1 <= job_arrival j2 < job_arrival j1
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1

t1 <= job_arrival j2 < job_arrival j1
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1

t1 <= job_arrival j2 < job_arrival j1
by rewrite (job_arrival_between_ge j2arr). Qed. (** We observe that, by construction, the sequence of arrivals is sorted by arrival times. To this end, we first define the order relation. *) Definition by_arrival_times (j1 j2 : Job) : bool := job_arrival j1 <= job_arrival j2. (** Trivially, the arrivals at any one point in time are ordered w.r.t. arrival times. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall t : instant, sorted by_arrival_times (arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall t : instant, sorted by_arrival_times (arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t: instant

sorted by_arrival_times (arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t: instant
AT_t: forall j : Job, j \in arrivals_at arr_seq t -> job_arrival j = t

sorted by_arrival_times (arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t: instant
j': Job
js: seq Job
AT_t: forall j : Job, j \in j' :: js -> job_arrival j = t

sorted by_arrival_times (j' :: js)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t: instant
j': Job
js: seq Job
AT_t: forall j : Job, j \in j' :: js -> job_arrival j = t
i: nat
LT: i < size js

by_arrival_times (nth j' (j' :: js) i) (nth j' js i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t: instant
j': Job
js: seq Job
AT_t: forall j : Job, j \in j' :: js -> job_arrival j = t
i: nat
LT: i < size js

nth j' js i \in j' :: js
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t: instant
j': Job
js: seq Job
AT_t: forall j : Job, j \in j' :: js -> job_arrival j = t
i: nat
LT: i < size js

nth j' js i \in js
by exact: mem_nth. Qed. (** By design, the list of arrivals in any interval is sorted. *)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall t1 t2 : instant, sorted by_arrival_times (arrivals_between arr_seq t1 t2)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq

forall t1 t2 : instant, sorted by_arrival_times (arrivals_between arr_seq t1 t2)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1, t2: instant

sorted by_arrival_times (arrivals_between arr_seq t1 t2)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1, t2: instant

sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)

sorted by_arrival_times (\cat_(t1<=t<t2.+1)arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2

sorted by_arrival_times (\cat_(t1<=t<t2.+1)arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2

sorted by_arrival_times (\cat_(t1<=i<t2)arrivals_at arr_seq i ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js

sorted by_arrival_times ((j :: js) ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js

path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
CAT: path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
sorted by_arrival_times ((j :: js) ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js

path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js

path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) (\cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js

path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js

sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t) -> path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
PATH_js: path by_arrival_times j js

path by_arrival_times j (j :: js)
by rewrite /path -/(path _ _ js) /by_arrival_times; apply /andP; split.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js

path by_arrival_times (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) (\cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js

path by_arrival_times (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) (\cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js

path by_arrival_times (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) (arrivals_at arr_seq t2)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'

path by_arrival_times (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) (j' :: js')
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'

transitive (T:=Job) by_arrival_times
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
by_arrival_times (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) j'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times j' (j' :: js')
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'

transitive (T:=Job) by_arrival_times
by rewrite /transitive/by_arrival_times; lia.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'

by_arrival_times (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) j'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times j' (j' :: js')
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'

by_arrival_times (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) j'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'

job_arrival (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) <= job_arrival j'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'

job_arrival (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) <= t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
L:= last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job

job_arrival L <= t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
L:= last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job
EX: exists t' : instant, L \in arrivals_at arr_seq t' /\ t1 <= t' < t2

job_arrival L <= t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
L:= last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job
t': instant
IN: L \in arrivals_at arr_seq t'
t1t': t1 <= t'
t't2: t' < t2

job_arrival L <= t2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
L:= last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job
t': instant
IN: L \in arrivals_at arr_seq t'
t1t': t1 <= t'
t't2: t' < t2

t' <= t2
by lia.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'

path by_arrival_times j' (j' :: js')
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'

path by_arrival_times j' (j' :: js')
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
PATH': path by_arrival_times j' js'

path by_arrival_times j' (j' :: js')
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
PATH': path by_arrival_times j' js'

(job_arrival j' <= job_arrival j') && path by_arrival_times j' js'
by apply /andP; split => //. } }
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
CAT: path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)

sorted by_arrival_times ((j :: js) ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
by move: CAT; rewrite /sorted A1 cat_cons {1}/path -/(path _ _ (js ++ _)) => /andP [_ CAT]. Qed. End ArrivalTimes. End ArrivalSequencePrefix. (** In this section, we establish a few auxiliary facts about the relation between the property of being scheduled and arrival predicates to facilitate automation. *) Section ScheduledImpliesArrives. (** Consider any type of jobs. *) Context {Job : JobType}. Context `{JobArrival Job}. (** Consider any kind of processor state model, ... *) Context {PState : ProcessorState Job}. (** ... any job arrival sequence with consistent arrivals, .... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq. (** ... and any schedule of this arrival sequence ... *) Variable sched : schedule PState. Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq. (** ... where jobs do not execute before their arrival. *) Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. (** Next, consider a job [j] ... *) Variable j : Job. (** ... which is scheduled at a time instant [t]. *) Variable t : instant. Hypothesis H_scheduled_at : scheduled_at sched j t. (** Then we show that [j] arrives in [arr_seq]. *)
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t

arrives_in arr_seq j
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t

arrives_in arr_seq j
by apply: H_jobs_come_from_arrival_sequence H_scheduled_at. Qed. (** Job [j] has arrived by time instant [t]. *)
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t

has_arrived j t
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t

has_arrived j t
by apply: H_jobs_must_arrive_to_execute H_scheduled_at. Qed. (** Finally, for any future time [t'], job [j] arrives before [t']. *)
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t

forall t' : nat, t < t' -> j \in arrivals_before arr_seq t'
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t

forall t' : nat, t < t' -> j \in arrivals_before arr_seq t'
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'

j \in arrivals_before arr_seq t'
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'

arrives_in arr_seq j
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'
arrived_between j 0 t'
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'

arrives_in arr_seq j
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'
arrived_between j 0 t'
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'

arrived_between j 0 t'
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'

arrived_between j 0 t'
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat

job_arrival j <= t
by apply: arrived_between_jobs_must_arrive_to_execute. Qed. End ScheduledImpliesArrives. (** We add some of the above lemmas to the "Hint Database" [basic_rt_facts], so the [auto] tactic will be able to use them. *) Global Hint Resolve arrivals_before_scheduled_at arrivals_uniq arrived_between_implies_in_arrivals arrived_between_jobs_must_arrive_to_execute arrives_in_jobs_come_from_arrival_sequence jobs_must_arrive_to_be_ready valid_schedule_implies_jobs_must_arrive_to_execute valid_schedule_jobs_come_from_arrival_sequence valid_schedule_jobs_must_be_ready_to_execute : basic_rt_facts.