From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
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.model.aggregate.workload.
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.model.aggregate.service_of_jobs.
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.model.service_of_jobs.
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]

(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
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.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]

(** * Service Received by Sets of Jobs in Ideal Uni-Processor Schedules *)

(** In this file, we establish a fact about the service received by _sets_ of
    jobs under ideal uni-processor schedule and the presence of idle times.  The
    lemma is currently specific to ideal uniprocessors only because of the lack
    of a general notion of idle time, which should be added in the near
    future. Conceptually, the fact holds for any [ideal_progress_proc_model].
    Once a general notion of idle time has been defined, this file should be
    generalized.  *)
Section IdealModelLemmas.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.

  (**  ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

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

  (** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_jobs_come_from_arrival_sequence:
    jobs_come_from_arrival_sequence sched arr_seq.
    
  (** ... where jobs do not execute before their arrival or after completion. *)
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

  (** Let [P] be any predicate over jobs. *)
  Variable P : pred Job.

  (** We prove that if the total service within some time interval <<[t1,t2)>>
      is smaller than <<t2 - t1>>, then there is an idle time instant [t ∈ [t1,t2)]. *)
  Lemma low_service_implies_existence_of_idle_time :
    forall t1 t2,
      service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
      exists t, t1 <= t < t2 /\ is_idle sched t.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
forall t1 t2 : instant,
service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat, t1 <= t < t2 /\ is_idle sched t
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
forall t1 t2 : instant,
service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat, t1 <= t < t2 /\ is_idle sched t
    intros ? ? SERV.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
exists t : nat, t1 <= t < t2 /\ is_idle sched t
    destruct (t1 <= t2) eqn:LE; last first.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
LE: (t1 <= t2) = false
exists t : nat, t1 <= t < t2 /\ is_idle sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
LE: (t1 <= t2) = true
exists t : nat, t1 <= t < t2 /\ is_idle sched t
    {
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
LE: (t1 <= t2) = false
exists t : nat, t1 <= t < t2 /\ is_idle sched t move: LE => /negP/negP; rewrite -ltnNge.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
t2 < t1 ->
exists t : nat, t1 <= t < t2 /\ is_idle sched t
      move => LT; apply ltnW in LT; rewrite -subn_eq0 in LT.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
LT: t2 - t1 == 0
exists t : nat, t1 <= t < t2 /\ is_idle sched t
      by move: LT => /eqP -> in SERV; rewrite ltn0 in SERV.
    }
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
LE: (t1 <= t2) = true
exists t : nat, t1 <= t < t2 /\ is_idle sched t
    have EX: exists δ, t2 = t1 + δ.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
LE: (t1 <= t2) = true
exists δ : nat, t2 = t1 + δ
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
LE: (t1 <= t2) = true
EX: exists δ : nat, t2 = t1 + δ
exists t : nat, t1 <= t < t2 /\ is_idle sched t
    {
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
LE: (t1 <= t2) = true
exists δ : nat, t2 = t1 + δ by exists (t2 - t1); rewrite subnKC // ltnW. }
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
LE: (t1 <= t2) = true
EX: exists δ : nat, t2 = t1 + δ
exists t : nat, t1 <= t < t2 /\ is_idle sched t
    move: EX => [δ EQ]; subst t2; clear LE.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ: nat
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 (t1 + δ)) t1
  (t1 + δ) < 
t1 + δ - t1
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
    rewrite {3}[t1 + δ]addnC -addnBA // subnn addn0 in SERV.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ: nat
SERV: service_of_jobs sched predT
  (arrivals_between arr_seq 0 (t1 + δ)) t1
  (t1 + δ) < δ
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
    rewrite /service_of_jobs exchange_big //= in SERV.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ: nat
SERV: \sum_(t1 <= j < 
t1 + δ)
   \sum_(i <- 
   arrivals_between arr_seq 0 
     (t1 + δ)) 
   service_at sched i j < δ
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
    apply sum_le_summation_range in SERV.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ: nat
SERV: exists x : nat,
  t1 <= x < t1 + δ /\
  \sum_(i <- 
  arrivals_between arr_seq 0 
    (t1 + δ)) 
  service_at sched i x = 0
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
    move: SERV => [x [/andP [GEx LEx] L]].
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
L: \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
   service_at sched i x = 0
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
    exists x; split; first by apply/andP; split.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
L: \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
   service_at sched i x = 0
is_idle sched x
    apply/negPn; apply/negP; intros NIDLE.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
L: \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
   service_at sched i x = 0
NIDLE: ~~ is_idle sched x
False
    unfold is_idle in NIDLE.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
L: \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
   service_at sched i x = 0
NIDLE: sched x != None
False
    destruct(sched x) eqn:SCHED; last by done.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
L: \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
   service_at sched i x = 0
s: Job
SCHED: sched x = Some s
NIDLE: Some s != None
False
    move: SCHED => /eqP SCHED; clear NIDLE; rewrite -scheduled_at_def/= in SCHED.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
L: \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
   service_at sched i x = 0
s: Job
SCHED: scheduled_at sched s x
False
    move: L => /eqP; rewrite sum_nat_eq0_nat filter_predT; move => /allP L.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
s: Job
SCHED: scheduled_at sched s x
L: {in arrivals_between arr_seq 0 (t1 + δ),
  forall x0 : Job, service_at sched x0 x == 0}
False
    specialize (L s); feed L.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
s: Job
SCHED: scheduled_at sched s x
L: s \in arrivals_between arr_seq 0 (t1 + δ) ->
(fun x0 : Job =>
 is_true (service_at sched x0 x == 0)) s
s \in arrivals_between arr_seq 0 (t1 + δ)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
s: Job
SCHED: scheduled_at sched s x
L: (fun x0 : Job =>
 is_true (service_at sched x0 x == 0)) s
False 
    {
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
s: Job
SCHED: scheduled_at sched s x
L: s \in arrivals_between arr_seq 0 (t1 + δ) ->
(fun x0 : Job =>
 is_true (service_at sched x0 x == 0)) s
s \in arrivals_between arr_seq 0 (t1 + δ) unfold arrivals_between.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
s: Job
SCHED: scheduled_at sched s x
L: s \in arrivals_between arr_seq 0 (t1 + δ) ->
(fun x0 : Job =>
 is_true (service_at sched x0 x == 0)) s
s \in \cat_(0<=t<t1 + δ)arrivals_at arr_seq t
      eapply arrived_between_implies_in_arrivals; eauto 2.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
s: Job
SCHED: scheduled_at sched s x
L: s \in arrivals_between arr_seq 0 (t1 + δ) ->
(fun x0 : Job =>
 is_true (service_at sched x0 x == 0)) s
arrived_between s 0 (t1 + δ)
      by apply H_jobs_must_arrive_to_execute in SCHED; apply leq_ltn_trans with x.
    }
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
s: Job
SCHED: scheduled_at sched s x
L: (fun x0 : Job =>
 is_true (service_at sched x0 x == 0)) s
False 
    move: SCHED L => /=.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
s: Job
scheduled_at sched s x ->
service_at sched s x == 0 -> False
    rewrite scheduled_at_def service_at_def => /eqP-> /eqP.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule (processor_state Job)
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
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
s: Job
(Some s == Some s) = 0 -> False
    by rewrite eqxx.
  Qed.

End IdealModelLemmas.