nonpreemptive

Require Export prosa.analysis.facts.preemption.task.nonpreemptive.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
Require Export prosa.analysis.facts.readiness.sequential.
Require Export prosa.analysis.definitions.tardiness.
Require Export prosa.implementation.facts.ideal_uni.prio_aware.
Require Export prosa.implementation.definitions.task.

(** ** Fully-Nonpreemptive Fixed-Priority Schedules  *)

(** In this section, we prove some facts about the fully-nonpreemptive
    preemption policy under fixed-priority schedules.

    Some lemmas in this file are not novel facts; they are used to uniform
    POET's certificates and minimize their verbosity. *)
Section Schedule.

  (** In this file, we adopt the Prosa standard implementation of jobs and tasks. *)
  Definition Task := concrete_task : eqType.
  Definition Job := concrete_job : eqType.

  (** Consider any valid arrival sequence, ... *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

  (** ... assume sequential readiness, ... *)
  Instance sequential_ready_instance : JobReady Job (ideal.processor_state Job) :=
    sequential_ready_instance arr_seq.

  (** ... and consider any fully-nonpreemptive, fixed-priority schedule. *)
  #[local] Existing Instance fully_nonpreemptive_job_model.
  #[local] Existing Instance NumericFPAscending.
  Definition sched := uni_schedule arr_seq.

  (** First, we show that only ready jobs execute. *)
  Lemma sched_jobs_must_be_ready_to_execute :
    jobs_must_be_ready_to_execute sched.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
jobs_must_be_ready_to_execute sched
  Proof.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
jobs_must_be_ready_to_execute sched
    move=> j t SCHED.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
job_ready sched j t
    apply jobs_must_be_ready => //.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
forall (t : instant) (s : seq Job) (j : Job),
choose_highest_prio_job t s = Some j -> j \in s
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
nonclairvoyant_readiness sequential_ready_instance
    -arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
forall (t : instant) (s : seq Job) (j : Job),
choose_highest_prio_job t s = Some j -> j \in s move=> tt ss jj IN.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
tt: instant
ss: seq Job
jj: Job
IN: choose_highest_prio_job tt ss = Some jj
jj \in ss
      rewrite  /choose_highest_prio_job in IN.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
tt: instant
ss: seq Job
jj: Job
IN: supremum (hep_job_at tt) ss = Some jj
jj \in ss
      by apply supremum_in in IN.
    -arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
nonclairvoyant_readiness sequential_ready_instance by apply sequential_readiness_nonclairvoyance.
  Qed.

  (** Next, we remark that such a schedule is valid. *)
  Remark sched_valid :
    valid_schedule sched arr_seq.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
valid_schedule sched arr_seq
  Proof.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
valid_schedule sched arr_seq
    split.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
jobs_come_from_arrival_sequence sched arr_seq
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
jobs_must_be_ready_to_execute sched
    -arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
jobs_come_from_arrival_sequence sched arr_seq apply np_schedule_jobs_from_arrival_sequence.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
forall (t : instant) (s : seq Job) (j : Job),
choose_highest_prio_job t s = Some j -> j \in s
      by move=> t ???; eapply (supremum_in (hep_job_at t)).
    -arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
jobs_must_be_ready_to_execute sched by apply sched_jobs_must_be_ready_to_execute.
  Qed.

  (** Next, we show that an unfinished job scheduled at time [t] is
      always scheduled at time [t+1] as well. Note that the validity of
      this fact also depends on which readiness model is used. *)
  Lemma sched_nonpreemptive_next:
    forall j t,
      scheduled_at sched j t ->
      ~~ completed_by sched j t.+1 ->
      scheduled_at sched j t.+1.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
forall (j : Job) (t : instant),
scheduled_at sched j t ->
~~ completed_by sched j t.+1 ->
scheduled_at sched j t.+1
  Proof.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
forall (j : Job) (t : instant),
scheduled_at sched j t ->
~~ completed_by sched j t.+1 ->
scheduled_at sched j t.+1
    move=> j t SCHED NCOMP.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
NCOMP: ~~ completed_by sched j t.+1
scheduled_at sched j t.+1
    have READY: job_ready sched j t by apply sched_jobs_must_be_ready_to_execute.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
NCOMP: ~~ completed_by sched j t.+1
READY: job_ready sched j t
scheduled_at sched j t.+1
    move: READY => /andP[/andP[ARR NC] /allP PRIOR].arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
NCOMP: ~~ completed_by sched j t.+1
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
scheduled_at sched j t.+1
    have SZ: 0 < service sched j t.+1.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
NCOMP: ~~ completed_by sched j t.+1
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
0 < service sched j t.+1
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
NCOMP: ~~ completed_by sched j t.+1
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SZ: 0 < service sched j t.+1
scheduled_at sched j t.+1
    {arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
NCOMP: ~~ completed_by sched j t.+1
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
0 < service sched j t.+1 apply scheduled_implies_nonzero_service; last  by simpl; exists t; split.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
NCOMP: ~~ completed_by sched j t.+1
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
ideal_progress_proc_model (processor_state Job)
      by apply ideal_proc_model_ensures_ideal_progress. }arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
NCOMP: ~~ completed_by sched j t.+1
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SZ: 0 < service sched j t.+1
scheduled_at sched j t.+1
    have SC: service sched j t.+1 < job_cost j by apply less_service_than_cost_is_incomplete.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
SCHED: scheduled_at sched j t
NCOMP: ~~ completed_by sched j t.+1
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SZ: 0 < service sched j t.+1
SC: service sched j t.+1 < job_cost j
scheduled_at sched j t.+1
    move: SCHED NCOMP; rewrite !scheduled_at_def /sched /uni_schedule /pmc_uni_schedule
                               /generic_schedule => /eqP SCHED NCOMP.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SZ: 0 < service sched j t.+1
SC: service sched j t.+1 < job_cost j
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
schedule_up_to
  (allocation_at arr_seq choose_highest_prio_job) None
  t.+1 t.+1 == Some j
    rewrite schedule_up_to_def {1}/allocation_at ifT; first by rewrite SCHED.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SZ: 0 < service sched j t.+1
SC: service sched j t.+1 < job_cost j
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
prev_job_nonpreemptive
  (schedule_up_to
     (allocation_at arr_seq choose_highest_prio_job)
     None t) t.+1
    rewrite /prev_job_nonpreemptive SCHED /job_preemptable /fully_nonpreemptive_job_model.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SZ: 0 < service sched j t.+1
SC: service sched j t.+1 < job_cost j
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
job_ready
  (schedule_up_to
     (allocation_at arr_seq choose_highest_prio_job)
     None t) j t.+1 &&
~~
((service
    (schedule_up_to
       (allocation_at arr_seq choose_highest_prio_job)
       None t) j t.+1 == 0)
 || (service
       (schedule_up_to
          (allocation_at arr_seq
             choose_highest_prio_job) None t) j t.+1 ==
     job.job_cost j))
    move: SC SZ; rewrite /uni_schedule /pmc_uni_schedule /generic_schedule.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
service sched j t.+1 < job_cost j ->
0 < service sched j t.+1 ->
job_ready
  (schedule_up_to
     (allocation_at arr_seq choose_highest_prio_job)
     None t) j t.+1 &&
~~
((service
    (schedule_up_to
       (allocation_at arr_seq choose_highest_prio_job)
       None t) j t.+1 == 0)
 || (service
       (schedule_up_to
          (allocation_at arr_seq
             choose_highest_prio_job) None t) j t.+1 ==
     job.job_cost j))
    set chp:= choose_highest_prio_job; set sut:= schedule_up_to.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
service sched j t.+1 < job_cost j ->
0 < service sched j t.+1 ->
job_ready (sut (allocation_at arr_seq chp) None t) j
  t.+1 &&
~~
((service (sut (allocation_at arr_seq chp) None t) j
    t.+1 == 0)
 || (service (sut (allocation_at arr_seq chp) None t)
       j t.+1 == job.job_cost j))
    replace (_ (_ (_ _ _) _ t) j t.+1) with (service sched j t.+1); last first.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
service sched j t.+1 =
service (sut (allocation_at arr_seq chp) None t) j
  t.+1
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
service sched j t.+1 < job_cost j ->
0 < service sched j t.+1 ->
job_ready (sut (allocation_at arr_seq chp) None t) j
  t.+1 &&
~~
((service sched j t.+1 == 0)
 || (service sched j t.+1 == job.job_cost j))
    {arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
service sched j t.+1 =
service (sut (allocation_at arr_seq chp) None t) j
  t.+1 rewrite /uni_schedule /pmc_uni_schedule /generic_schedule /service
              /service_during /service_at; apply eq_big_nat => i H.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
i: nat
H: 0 <= i < t.+1
service_in j (sched i) =
service_in j
  (sut (allocation_at arr_seq chp) None t i)
      replace (_ (_ _ _) _ t i) with (sut (allocation_at arr_seq chp) None i i) => //.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
i: nat
H: 0 <= i < t.+1
sut (allocation_at arr_seq chp) None i i =
sut (allocation_at arr_seq chp) None t i
      by apply schedule_up_to_prefix_inclusion. }arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
service sched j t.+1 < job_cost j ->
0 < service sched j t.+1 ->
job_ready (sut (allocation_at arr_seq chp) None t) j
  t.+1 &&
~~
((service sched j t.+1 == 0)
 || (service sched j t.+1 == job.job_cost j))
    move=> SC SZ; apply /andP.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
job_ready (sut (allocation_at arr_seq chp) None t) j
  t.+1 /\
~~
((service sched j t.+1 == 0)
 || (service sched j t.+1 == job.job_cost j))
    split; last by apply /norP; split; [rewrite -lt0n|move:SC; rewrite ltn_neqAle=> /andP[??]].arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
job_ready (sut (allocation_at arr_seq chp) None t) j
  t.+1
    apply /andP; split; [apply /andP; split; [by unfold has_arrived in *; lia|]|].arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
~~
completed_by (sut (allocation_at arr_seq chp) None t)
  j t.+1
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
prior_jobs_complete arr_seq
  (sut (allocation_at arr_seq chp) None t) j t.+1
    {arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
~~
completed_by (sut (allocation_at arr_seq chp) None t)
  j t.+1 unfold completed_by in *; rewrite <- ltnNge in *.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: service sched j t < job.job_cost j
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job,
  job.job_cost x <= service sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: service
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1 < job.job_cost j
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
service (sut (allocation_at arr_seq chp) None t) j
  t.+1 < job.job_cost j
      replace (_ _ j _) with (service (fun t=> sut (allocation_at arr_seq chp) None t t) j t.+1)=> //.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: service sched j t < job.job_cost j
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job,
  job.job_cost x <= service sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: service
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1 < job.job_cost j
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
service
  (fun t : instant =>
   sut (allocation_at arr_seq chp) None t t) j t.+1 =
service (sut (allocation_at arr_seq chp) None t) j
  t.+1
      rewrite /service /service_during //=; apply eq_big_nat.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: service sched j t < job.job_cost j
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job,
  job.job_cost x <= service sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: service
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1 < job.job_cost j
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
forall i : nat,
0 <= i < t.+1 ->
service_at
  (fun t : instant =>
   sut (allocation_at arr_seq chp) None t t) j i =
service_at (sut (allocation_at arr_seq chp) None t) j
  i
      move=> t' /andP[GEQ0 LEQt]; rewrite /service_at.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: service sched j t < job.job_cost j
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job,
  job.job_cost x <= service sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: service
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1 < job.job_cost j
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
t': nat
GEQ0: 0 <= t'
LEQt: t' < t.+1
service_in j
  (sut (allocation_at arr_seq chp) None t' t') =
service_in j
  (sut (allocation_at arr_seq chp) None t t')
      replace (_ _  _ _ _) with (sut (allocation_at arr_seq chp) None t t')=> //.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: service sched j t < job.job_cost j
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job,
  job.job_cost x <= service sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: service
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1 < job.job_cost j
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
t': nat
GEQ0: 0 <= t'
LEQt: t' < t.+1
sut (allocation_at arr_seq chp) None t t' =
sut (allocation_at arr_seq chp) None t' t'
      by symmetry; apply schedule_up_to_prefix_inclusion; lia. }arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
prior_jobs_complete arr_seq
  (sut (allocation_at arr_seq chp) None t) j t.+1
    {arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
prior_jobs_complete arr_seq
  (sut (allocation_at arr_seq chp) None t) j t.+1 apply /allP => j' IN; apply (leq_trans (PRIOR j' IN)).arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
j': Job
IN: j'
  \in task_arrivals_before arr_seq
        (concept.job_task j) 
        (job.job_arrival j)
service sched j' t <=
service (sut (allocation_at arr_seq chp) None t) j'
  t.+1
      rewrite /service /service_during big_nat_recr //= -(addn0  (\sum_(0 <= _ < t) _)).arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
j': Job
IN: j'
  \in task_arrivals_before arr_seq
        (concept.job_task j) 
        (job.job_arrival j)
\sum_(0 <= H < t) service_at sched j' H + 0 <=
\sum_(0 <= i < t)
   service_at (sut (allocation_at arr_seq chp) None t)
     j' i +
service_at (sut (allocation_at arr_seq chp) None t) j'
  t
      apply leq_add => //; apply eq_leq, eq_big_nat.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
j': Job
IN: j'
  \in task_arrivals_before arr_seq
        (concept.job_task j) 
        (job.job_arrival j)
forall i : nat,
0 <= i < t ->
service_at sched j' i =
service_at (sut (allocation_at arr_seq chp) None t) j'
  i
      move=> t' /andP[GEQ0 LEQt].arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
j': Job
IN: j'
  \in task_arrivals_before arr_seq
        (concept.job_task j) 
        (job.job_arrival j)
t': nat
GEQ0: 0 <= t'
LEQt: t' < t
service_at sched j' t' =
service_at (sut (allocation_at arr_seq chp) None t) j'
  t'
      rewrite /service_at /sched /uni_schedule /pmc_uni_schedule /generic_schedule.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
j': Job
IN: j'
  \in task_arrivals_before arr_seq
        (concept.job_task j) 
        (job.job_arrival j)
t': nat
GEQ0: 0 <= t'
LEQt: t' < t
service_in j'
  (schedule_up_to
     (allocation_at arr_seq choose_highest_prio_job)
     None t' t') =
service_in j'
  (sut (allocation_at arr_seq chp) None t t')
      replace (_ (_ _ _) _ t' t') with (sut (allocation_at arr_seq chp) None t t') => //.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
ARR: has_arrived j t
NC: ~~ completed_by sched j t
PRIOR: {in task_arrivals_before arr_seq
      (concept.job_task j) 
      (job.job_arrival j),
  forall x : Job, completed_by sched x t}
SCHED: schedule_up_to
  (allocation_at arr_seq
     choose_highest_prio_job) None t t =
Some j
NCOMP: ~~
completed_by
  (fun t : instant =>
   schedule_up_to
     (allocation_at arr_seq
        choose_highest_prio_job) None t t) j
  t.+1
chp:= choose_highest_prio_job: instant -> seq Job -> option Job
sut:= schedule_up_to: PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
SC: service sched j t.+1 < job_cost j
SZ: 0 < service sched j t.+1
j': Job
IN: j'
  \in task_arrivals_before arr_seq
        (concept.job_task j) 
        (job.job_arrival j)
t': nat
GEQ0: 0 <= t'
LEQt: t' < t
sut (allocation_at arr_seq chp) None t t' =
schedule_up_to
  (allocation_at arr_seq choose_highest_prio_job) None
  t' t'
      by symmetry; apply schedule_up_to_prefix_inclusion; lia. }
  Qed.

  (** Using the lemma above, we show that the schedule is nonpreemptive. *)
  Lemma sched_nonpreemptive :
    nonpreemptive_schedule (uni_schedule arr_seq).arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
nonpreemptive_schedule (uni_schedule arr_seq)
  Proof.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
nonpreemptive_schedule (uni_schedule arr_seq)
    rewrite /nonpreemptive_schedule.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
forall (j : Job) (t t' : instant),
t <= t' ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
    move=> j t; elim=> [|t' IHt']; first by move=> t'; have->: t = 0 by lia.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
t': nat
IHt': t <= t' ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
t <= t'.+1 ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t'.+1 ->
scheduled_at (uni_schedule arr_seq) j t'.+1
    move=> LEQ SCHED NCOMP.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
t': nat
IHt': t <= t' ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
LEQ: t <= t'.+1
SCHED: scheduled_at (uni_schedule arr_seq) j t
NCOMP: ~~ completed_by (uni_schedule arr_seq) j t'.+1
scheduled_at (uni_schedule arr_seq) j t'.+1
    destruct (ltngtP t t'.+1) as [LT | _ | EQ] => //.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
t': nat
IHt': t <= t' ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
LEQ: true
SCHED: scheduled_at (uni_schedule arr_seq) j t
NCOMP: ~~ completed_by (uni_schedule arr_seq) j t'.+1
LT: t < t'.+1
scheduled_at (uni_schedule arr_seq) j t'.+1
    feed_n 3 IHt'=> //.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
t': nat
IHt': ~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
LEQ: true
SCHED: scheduled_at (uni_schedule arr_seq) j t
NCOMP: ~~ completed_by (uni_schedule arr_seq) j t'.+1
LT: t < t'.+1
~~ completed_by (uni_schedule arr_seq) j t'
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
t': nat
IHt': scheduled_at (uni_schedule arr_seq) j t'
LEQ: true
SCHED: scheduled_at (uni_schedule arr_seq) j t
NCOMP: ~~ completed_by (uni_schedule arr_seq) j t'.+1
LT: t < t'.+1
scheduled_at (uni_schedule arr_seq) j t'.+1
    {arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
t': nat
IHt': ~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
LEQ: true
SCHED: scheduled_at (uni_schedule arr_seq) j t
NCOMP: ~~ completed_by (uni_schedule arr_seq) j t'.+1
LT: t < t'.+1
~~ completed_by (uni_schedule arr_seq) j t' specialize (completion_monotonic sched j t' t'.+1) => MONO.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
t': nat
IHt': ~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
LEQ: true
SCHED: scheduled_at (uni_schedule arr_seq) j t
NCOMP: ~~ completed_by (uni_schedule arr_seq) j t'.+1
LT: t < t'.+1
MONO: t' <= t'.+1 ->
completed_by sched j t' ->
completed_by sched j t'.+1
~~ completed_by (uni_schedule arr_seq) j t'
      feed MONO; first by lia.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
t': nat
IHt': ~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
LEQ: true
SCHED: scheduled_at (uni_schedule arr_seq) j t
NCOMP: ~~ completed_by (uni_schedule arr_seq) j t'.+1
LT: t < t'.+1
MONO: completed_by sched j t' ->
completed_by sched j t'.+1
~~ completed_by (uni_schedule arr_seq) j t'
      by apply contra in MONO. }arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
j: Job
t: instant
t': nat
IHt': scheduled_at (uni_schedule arr_seq) j t'
LEQ: true
SCHED: scheduled_at (uni_schedule arr_seq) j t
NCOMP: ~~ completed_by (uni_schedule arr_seq) j t'.+1
LT: t < t'.+1
scheduled_at (uni_schedule arr_seq) j t'.+1
    by apply sched_nonpreemptive_next.
  Qed.

  (** Finally, we show that the fixed-priority policy is respected at each preemption point. *)
  Lemma respects_policy_at_preemption_point_np :
    respects_FP_policy_at_preemption_point arr_seq sched (NumericFPAscending Task).arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
respects_FP_policy_at_preemption_point arr_seq sched
  (NumericFPAscending Task)
  Proof.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
respects_FP_policy_at_preemption_point arr_seq sched
  (NumericFPAscending Task)
    apply schedule_respects_policy => //.arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
nonclairvoyant_readiness sequential_ready_instance
    by apply sequential_readiness_nonclairvoyance.
  Qed.

End Schedule.