preemption.v

Require Export prosa.model.schedule.priority_driven.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]
Require Export prosa.analysis.facts.model.ideal.schedule.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.analysis.facts.behavior.completion.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]

(** In this section, we establish two basic facts about preemption times. *)
Section PreemptionTimes.
  
  (** Consider any type of jobs. *)
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** In addition, we assume the existence of a function mapping a job and
      its progress to a boolean value saying whether this job is
      preemptable at its current point of execution. *)
  Context `{JobPreemptable Job}.

  (** Consider any arrival sequence with consistent arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

  (** Next, consider any ideal uniprocessor schedule of this arrival sequence... *)
  Variable sched : schedule (ideal.processor_state Job).

  (** ...where, jobs come from the arrival sequence. *)
  Hypothesis H_jobs_come_from_arrival_sequence:
    jobs_come_from_arrival_sequence sched arr_seq.

  (** Consider a valid preemption model. *)
  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched. 

  (**  We show that time 0 is a preemption time. *)
  Lemma zero_is_pt: preemption_time sched 0.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
preemption_time sched 0
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
preemption_time sched 0
    unfold preemption_time.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
match sched 0 with
| Some j => job_preemptable j (service sched j 0)
| None => true
end
    case SCHED: (sched 0) => [j | ]; last by done.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
j: Job
SCHED: sched 0 = Some j
job_preemptable j (service sched j 0)
    move: (SCHED) => /eqP; rewrite -scheduled_at_def; move => ARR.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
j: Job
SCHED: sched 0 = Some j
ARR: scheduled_at sched j 0
job_preemptable j (service sched j 0)
    apply H_jobs_come_from_arrival_sequence in ARR.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
j: Job
SCHED: sched 0 = Some j
ARR: arrives_in arr_seq j
job_preemptable j (service sched j 0)
    rewrite /service /service_during big_geq; last by done.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
j: Job
SCHED: sched 0 = Some j
ARR: arrives_in arr_seq j
job_preemptable j 0
    by move: (H_valid_preemption_model j ARR) => [PP _].
  Qed.
  (** Also, we show that the first instant of execution is a preemption time. *)
  Lemma first_moment_is_pt:
    forall j prt,
      arrives_in arr_seq j ->
      ~~ scheduled_at sched j prt ->
      scheduled_at sched j prt.+1 ->
      preemption_time sched prt.+1.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
forall (j : Job) (prt : instant),
arrives_in arr_seq j ->
~~ scheduled_at sched j prt ->
scheduled_at sched j prt.+1 ->
preemption_time sched prt.+1
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
forall (j : Job) (prt : instant),
arrives_in arr_seq j ->
~~ scheduled_at sched j prt ->
scheduled_at sched j prt.+1 ->
preemption_time sched prt.+1
    intros s pt ARR NSCHED SCHED.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
pt: instant
ARR: arrives_in arr_seq s
NSCHED: ~~ scheduled_at sched s pt
SCHED: scheduled_at sched s pt.+1
preemption_time sched pt.+1
    unfold preemption_time.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
pt: instant
ARR: arrives_in arr_seq s
NSCHED: ~~ scheduled_at sched s pt
SCHED: scheduled_at sched s pt.+1
match sched pt.+1 with
| Some j => job_preemptable j (service sched j pt.+1)
| None => true
end
    move: (SCHED); rewrite scheduled_at_def; move => /eqP SCHED2; rewrite SCHED2; clear SCHED2.Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobPreemptable Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule (ideal.processor_state Job)
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
pt: instant
ARR: arrives_in arr_seq s
NSCHED: ~~ scheduled_at sched s pt
SCHED: scheduled_at sched s pt.+1
job_preemptable s (service sched s pt.+1)
    by move: (H_valid_preemption_model s ARR) => [_ [_ [_ P]]]; apply P.
  Qed.

End PreemptionTimes.

(** In this section, we prove a lemma relating scheduling and preemption times. *)
Section PreemptionFacts.

  (** Consider any type of jobs. *)
  Context {Job : JobType}.
  Context `{Arrival : JobArrival Job}.
  Context `{Cost : JobCost Job}.
  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.

  (** Consider any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.

  (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
  Variable sched : schedule (ideal.processor_state Job).
  
  (** ...and, assume that the schedule is valid. *)
  Hypothesis H_sched_valid : valid_schedule sched arr_seq.

  (** In addition, we assume the existence of a function mapping jobs to their preemption points ... *)
  Context `{JobPreemptable Job}.

  (** ... and assume that it defines a valid preemption model. *)
  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.

  (** We prove that every nonpreemptive segment always begins with a preemption time. *)
  Lemma scheduling_of_any_segment_starts_with_preemption_time:
    forall j t,
      scheduled_at sched j t ->
      exists pt,
        job_arrival j <= pt <= t /\
          preemption_time sched pt /\
          (forall t', pt <= t' <= t -> scheduled_at sched j t').Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists pt : nat,
  job_arrival j <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched j t')
  Proof.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists pt : nat,
  job_arrival j <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched j t')
    intros s t SCHEDst.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
    have EX: exists t', (t' <= t) && (scheduled_at sched s t')
                   && (all (fun t'' => scheduled_at sched  s t'') (index_iota t' t.+1 )).Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
exists t' : nat,
  (t' <= t) && scheduled_at sched s t' &&
  all [eta scheduled_at sched s] (index_iota t' t.+1)
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
EX: exists t' : nat,
  (t' <= t) && scheduled_at sched s t' &&
  all [eta scheduled_at sched s]
    (index_iota t' t.+1)
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
    {Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
exists t' : nat,
  (t' <= t) && scheduled_at sched s t' &&
  all [eta scheduled_at sched s] (index_iota t' t.+1) exists t.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
(t <= t) && scheduled_at sched s t &&
all [eta scheduled_at sched s] (index_iota t t.+1) apply/andP; split; [ by apply/andP; split | ].Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
all [eta scheduled_at sched s] (index_iota t t.+1)
      apply/allP; intros t'.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
t': nat_eqType
t' \in index_iota t t.+1 -> scheduled_at sched s t'
      by rewrite mem_index_iota ltnS -eqn_leq; move => /eqP <-.  
    }Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
EX: exists t' : nat,
  (t' <= t) && scheduled_at sched s t' &&
  all [eta scheduled_at sched s]
    (index_iota t' t.+1)
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
    have MATE : jobs_must_arrive_to_execute sched by rt_eauto.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
EX: exists t' : nat,
  (t' <= t) && scheduled_at sched s t' &&
  all [eta scheduled_at sched s]
    (index_iota t' t.+1)
MATE: jobs_must_arrive_to_execute sched
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t') 
    move :  (H_sched_valid) =>  [COME_ARR READY].Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
EX: exists t' : nat,
  (t' <= t) && scheduled_at sched s t' &&
  all [eta scheduled_at sched s]
    (index_iota t' t.+1)
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
    have MIN := ex_minnP EX.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
EX: exists t' : nat,
  (t' <= t) && scheduled_at sched s t' &&
  all [eta scheduled_at sched s]
    (index_iota t' t.+1)
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
MIN: ex_minn_spec
  (fun t' : nat =>
   (t' <= t) && scheduled_at sched s t' &&
   all [eta scheduled_at sched s]
     (index_iota t' t.+1))
  (ex_minn
     (P:=fun t' : nat =>
         (t' <= t) && scheduled_at sched s t' &&
         all [eta scheduled_at sched s]
           (index_iota t' t.+1)) EX)
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t') 
    move: MIN => [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt <= t
SCHEDsmpt: scheduled_at sched s mpt
ALL: {in index_iota mpt t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt <= n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
    destruct mpt.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
    -Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t') exists 0; repeat split.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
job_arrival s <= 0 <= t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
preemption_time sched 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
forall t' : nat,
0 <= t' <= t -> scheduled_at sched s t'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
      +Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
job_arrival s <= 0 <= t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
preemption_time sched 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
forall t' : nat,
0 <= t' <= t -> scheduled_at sched s t'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t') by apply/andP; split => //; apply MATE.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
preemption_time sched 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
forall t' : nat,
0 <= t' <= t -> scheduled_at sched s t'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
      +Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
preemption_time sched 0
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
forall t' : nat,
0 <= t' <= t -> scheduled_at sched s t'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')  eapply (zero_is_pt arr_seq); eauto 2.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
forall t' : nat,
0 <= t' <= t -> scheduled_at sched s t'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
      +Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
LT1: 0 <= t
SCHEDsmpt: scheduled_at sched s 0
ALL: {in index_iota 0 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
0 <= n
forall t' : nat,
0 <= t' <= t -> scheduled_at sched s t'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t') by intros; apply ALL; rewrite mem_iota subn0 add0n ltnS.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
    -Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t') have NSCHED: ~~ scheduled_at sched  s mpt.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
~~ scheduled_at sched s mpt
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
      {Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
~~ scheduled_at sched s mpt apply/negP; intros SCHED.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
False
        enough (F : mpt < mpt); first by rewrite ltnn in F.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
mpt < mpt
        apply MIN.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
(mpt <= t) && scheduled_at sched s mpt &&
all [eta scheduled_at sched s] (index_iota mpt t.+1)
        apply/andP; split; [by apply/andP; split; [ apply ltnW | ] | ].Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
all [eta scheduled_at sched s] (index_iota mpt t.+1)
        apply/allP; intros t'.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
t': nat_eqType
t' \in index_iota mpt t.+1 -> scheduled_at sched s t'
        rewrite mem_index_iota; move => /andP [GE LE].Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
t': nat_eqType
GE: mpt <= t'
LE: t' < t.+1
scheduled_at sched s t'
        move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LT].Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
t': nat_eqType
LE: t' < t.+1
EQ: mpt = t'
scheduled_at sched s t'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
t': nat_eqType
LE: t' < t.+1
LT: mpt < t'
scheduled_at sched s t'
        -Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
t': nat_eqType
LE: t' < t.+1
EQ: mpt = t'
scheduled_at sched s t'
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
t': nat_eqType
LE: t' < t.+1
LT: mpt < t'
scheduled_at sched s t' by subst t'.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
t': nat_eqType
LE: t' < t.+1
LT: mpt < t'
scheduled_at sched s t' 
        -Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
SCHED: scheduled_at sched s mpt
t': nat_eqType
LE: t' < t.+1
LT: mpt < t'
scheduled_at sched s t' by apply ALL; rewrite mem_index_iota; apply/andP; split. 
      }Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')         
      have PP: preemption_time sched mpt.+1 by eapply (first_moment_is_pt arr_seq)  with (j := s); eauto 2.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
exists pt : nat,
  job_arrival s <= pt <= t /\
  preemption_time sched pt /\
  (forall t' : nat,
   pt <= t' <= t -> scheduled_at sched s t')
      exists mpt.+1; repeat split; try done.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
job_arrival s <= mpt.+1 <= t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
forall t' : nat,
mpt < t' <= t -> scheduled_at sched s t'
      +Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
job_arrival s <= mpt.+1 <= t
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
forall t' : nat,
mpt < t' <= t -> scheduled_at sched s t' apply/andP; split; last by done.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
job_arrival s <= mpt.+1
Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
forall t' : nat,
mpt < t' <= t -> scheduled_at sched s t'
       by apply MATE in SCHEDsmpt.Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
forall t' : nat,
mpt < t' <= t -> scheduled_at sched s t'
      +Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
forall t' : nat,
mpt < t' <= t -> scheduled_at sched s t' move => t' /andP [GE LE].Job: JobType
Arrival: JobArrival Job
Cost: JobCost Job
H: JobReady Job (ideal.processor_state Job)
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H0: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
s: Job
t: instant
SCHEDst: scheduled_at sched s t
MATE: jobs_must_arrive_to_execute sched
COME_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
READY: jobs_must_be_ready_to_execute sched
mpt: nat
LT1: mpt < t
SCHEDsmpt: scheduled_at sched s mpt.+1
ALL: {in index_iota mpt.+1 t.+1,
  forall x : nat_eqType, scheduled_at sched s x}
MIN: forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
  (index_iota n t.+1) -> 
mpt < n
NSCHED: ~~ scheduled_at sched s mpt
PP: preemption_time sched mpt.+1
t': nat
GE: mpt < t'
LE: t' <= t
scheduled_at sched s t'
        by apply ALL; rewrite mem_index_iota; apply/andP; split.
  Qed.

End PreemptionFacts.