Library prosa.implementation.facts.ideal_uni.preemption_aware


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)


Require Export prosa.implementation.facts.generic_schedule.
Require Export prosa.implementation.definitions.ideal_uni_scheduler.
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Export prosa.model.schedule.limited_preemptive.

Properties of the Preemption-Aware Ideal Uniprocessor Scheduler

This file establishes facts about the reference model of a preemption-model-aware ideal uniprocessor scheduler.
The following results assume ideal uniprocessor schedules.
Consider any type of jobs with costs and arrival times, ...
  Context {Job : JobType} {JC : JobCost Job} {JA : JobArrival Job}.

... in the context of an ideal uniprocessor model.
Suppose we are given a consistent arrival sequence of such jobs, ...
... a non-clairvoyant readiness model, ...
... and a preemption model.
  Context `{JobPreemptable Job}.

For any given job selection policy ...
... consider the schedule produced by the preemption-aware scheduler for the policy induced by [choose_job].
To begin with, we establish that the preemption-aware scheduler does not induce non-work-conserving behavior.
  Section WorkConservation.

If [choose_job] does not voluntarily idle the processor, ...
    Hypothesis H_non_idling:
       t s,
        choose_job t s = idle_state s = [::].

... then we can establish work-conservation.
First, we observe that [allocation_at] yields [idle_state] only if there are no backlogged jobs.
    Lemma allocation_at_idle:
       sched t,
        allocation_at arr_seq choose_job sched t = idle_state
        jobs_backlogged_at arr_seq sched t = [::].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 60)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  ============================
  forall (sched : schedule.schedule (processor_state Job)) (t : instant),
  allocation_at arr_seq choose_job sched t = idle_state ->
  jobs_backlogged_at arr_seq sched t = [::]

----------------------------------------------------------------------------- *)


    Proof.
      movesched t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 62)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  sched : schedule.schedule (processor_state Job)
  t : instant
  ============================
  allocation_at arr_seq choose_job sched t = idle_state ->
  jobs_backlogged_at arr_seq sched t = [::]

----------------------------------------------------------------------------- *)


      elim: t ⇒ [|t _]; first by apply H_non_idling.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 74)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  sched : schedule.schedule (processor_state Job)
  t : nat
  ============================
  allocation_at arr_seq choose_job sched t.+1 = idle_state ->
  jobs_backlogged_at arr_seq sched t.+1 = [::]

----------------------------------------------------------------------------- *)


      rewrite /allocation_at /prev_job_nonpreemptive.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 90)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  sched : schedule.schedule (processor_state Job)
  t : nat
  ============================
  (if
    match sched t with
    | Some j => ~~ job_preemptable j (service sched j t.+1)
    | None => false
    end
   then sched t.+1.-1
   else choose_job t.+1 (jobs_backlogged_at arr_seq sched t.+1)) = idle_state ->
  jobs_backlogged_at arr_seq sched t.+1 = [::]

----------------------------------------------------------------------------- *)


      elim: (sched t) ⇒ [j'|]; last by apply H_non_idling.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 99)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  sched : schedule.schedule (processor_state Job)
  t : nat
  j' : Job
  ============================
  (if ~~ job_preemptable j' (service sched j' t.+1)
   then Some j'
   else choose_job t.+1 (jobs_backlogged_at arr_seq sched t.+1)) = idle_state ->
  jobs_backlogged_at arr_seq sched t.+1 = [::]

----------------------------------------------------------------------------- *)


      rewrite if_neg.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 109)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  sched : schedule.schedule (processor_state Job)
  t : nat
  j' : Job
  ============================
  (if job_preemptable j' (service sched j' t.+1)
   then choose_job t.+1 (jobs_backlogged_at arr_seq sched t.+1)
   else Some j') = idle_state -> jobs_backlogged_at arr_seq sched t.+1 = [::]

----------------------------------------------------------------------------- *)


      elim: (job_preemptable j' (service sched j' t.+1)); first by apply H_non_idling.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 126)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  sched : schedule.schedule (processor_state Job)
  t : nat
  j' : Job
  ============================
  Some j' = idle_state -> jobs_backlogged_at arr_seq sched t.+1 = [::]

----------------------------------------------------------------------------- *)


      by discriminate.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

As a stepping stone, we observe that the generated schedule is idle at a time [t] only if there are no backlogged jobs.
    Lemma idle_schedule_no_backlogged_jobs:
       t,
        is_idle schedule t
        jobs_backlogged_at arr_seq schedule t = [::].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 71)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  ============================
  forall t : instant,
  is_idle schedule t -> jobs_backlogged_at arr_seq schedule t = [::]

----------------------------------------------------------------------------- *)


    Proof.
      movet.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 72)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  ============================
  is_idle schedule t -> jobs_backlogged_at arr_seq schedule t = [::]

----------------------------------------------------------------------------- *)


      rewrite /is_idle /schedule /np_uni_schedule /generic_schedule ⇒ /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 118)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t t = None ->
  jobs_backlogged_at arr_seq
    (fun t0 : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) t = [::]

----------------------------------------------------------------------------- *)


      moveNONE.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 119)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  ============================
  jobs_backlogged_at arr_seq
    (fun t0 : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) t = [::]

----------------------------------------------------------------------------- *)


move: (NONE).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 120)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t t = None ->
  jobs_backlogged_at arr_seq
    (fun t0 : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) t = [::]

----------------------------------------------------------------------------- *)


      rewrite schedule_up_to_defIDLE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 128)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  IDLE : allocation_at arr_seq choose_job
           match t with
           | 0 => empty_schedule None
           | t'.+1 =>
               schedule_up_to (allocation_at arr_seq choose_job) None t'
           end t = None
  ============================
  jobs_backlogged_at arr_seq
    (fun t0 : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) t = [::]

----------------------------------------------------------------------------- *)


      apply allocation_at_idle in IDLE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 130)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  IDLE : jobs_backlogged_at arr_seq
           match t with
           | 0 => empty_schedule None
           | t'.+1 =>
               schedule_up_to (allocation_at arr_seq choose_job) None t'
           end t = [::]
  ============================
  jobs_backlogged_at arr_seq
    (fun t0 : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) t = [::]

----------------------------------------------------------------------------- *)


      rewrite -IDLE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 132)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  IDLE : jobs_backlogged_at arr_seq
           match t with
           | 0 => empty_schedule None
           | t'.+1 =>
               schedule_up_to (allocation_at arr_seq choose_job) None t'
           end t = [::]
  ============================
  jobs_backlogged_at arr_seq
    (fun t0 : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) t =
  jobs_backlogged_at arr_seq
    match t with
    | 0 => empty_schedule None
    | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
    end t

----------------------------------------------------------------------------- *)


      apply backlogged_jobs_prefix_invariance with (h := t.+1) ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 140)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  IDLE : jobs_backlogged_at arr_seq
           match t with
           | 0 => empty_schedule None
           | t'.+1 =>
               schedule_up_to (allocation_at arr_seq choose_job) None t'
           end t = [::]
  ============================
  identical_prefix
    (fun t0 : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t0 t0)
    match t with
    | 0 => empty_schedule None
    | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
    end t.+1

----------------------------------------------------------------------------- *)


      rewrite /identical_prefixx.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  IDLE : jobs_backlogged_at arr_seq
           match t with
           | 0 => empty_schedule None
           | t'.+1 =>
               schedule_up_to (allocation_at arr_seq choose_job) None t'
           end t = [::]
  x : nat
  ============================
  x < t.+1 ->
  schedule_up_to (allocation_at arr_seq choose_job) None x x =
  match t with
  | 0 => empty_schedule None
  | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
  end x

----------------------------------------------------------------------------- *)


      rewrite ltnS leq_eqVlt ⇒ /orP [/eqP ->|LT]; last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 253)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  IDLE : jobs_backlogged_at arr_seq
           match t with
           | 0 => empty_schedule None
           | t'.+1 =>
               schedule_up_to (allocation_at arr_seq choose_job) None t'
           end t = [::]
  x : nat
  LT : x < t
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None x x =
  match t with
  | 0 => empty_schedule None
  | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
  end x

subgoal 2 (ID 252) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t t =
 match t with
 | 0 => empty_schedule None
 | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
 end t

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 253)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  IDLE : jobs_backlogged_at arr_seq
           match t with
           | 0 => empty_schedule None
           | t'.+1 =>
               schedule_up_to (allocation_at arr_seq choose_job) None t'
           end t = [::]
  x : nat
  LT : x < t
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None x x =
  match t with
  | 0 => empty_schedule None
  | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
  end x

----------------------------------------------------------------------------- *)


elim: t LT IDLE NONE ⇒ // ⇒ h IH LT_x IDLE NONE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 331)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  x, h : nat
  IH : x < h ->
       jobs_backlogged_at arr_seq
         match h with
         | 0 => empty_schedule None
         | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
         end h = [::] ->
       schedule_up_to (allocation_at arr_seq choose_job) None h h = None ->
       schedule_up_to (allocation_at arr_seq choose_job) None x x =
       match h with
       | 0 => empty_schedule None
       | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
       end x
  LT_x : x < h.+1
  IDLE : jobs_backlogged_at arr_seq
           (schedule_up_to (allocation_at arr_seq choose_job) None h) h.+1 =
         [::]
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None h.+1 h.+1 =
         None
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None x x =
  schedule_up_to (allocation_at arr_seq choose_job) None h x

----------------------------------------------------------------------------- *)


        by apply schedule_up_to_prefix_inclusion.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 252) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t t =
 match t with
 | 0 => empty_schedule None
 | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
 end t

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 252)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  IDLE : jobs_backlogged_at arr_seq
           match t with
           | 0 => empty_schedule None
           | t'.+1 =>
               schedule_up_to (allocation_at arr_seq choose_job) None t'
           end t = [::]
  x : nat
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t t =
  match t with
  | 0 => empty_schedule None
  | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
  end t

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 252)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  t : instant
  NONE : schedule_up_to (allocation_at arr_seq choose_job) None t t = None
  IDLE : jobs_backlogged_at arr_seq
           match t with
           | 0 => empty_schedule None
           | t'.+1 =>
               schedule_up_to (allocation_at arr_seq choose_job) None t'
           end t = [::]
  x : nat
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t t =
  match t with
  | 0 => empty_schedule None
  | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t'
  end t

----------------------------------------------------------------------------- *)


elim: t IDLE NONE ⇒ [IDLE _| t' _ _ ->]; last by rewrite schedule_up_to_empty.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 357)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  x : nat
  IDLE : jobs_backlogged_at arr_seq (empty_schedule None) 0 = [::]
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None 0 0 =
  empty_schedule None 0

----------------------------------------------------------------------------- *)


        rewrite /schedule_up_to replace_at_def.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 378)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  x : nat
  IDLE : jobs_backlogged_at arr_seq (empty_schedule None) 0 = [::]
  ============================
  allocation_at arr_seq choose_job (empty_schedule None) 0 =
  empty_schedule None 0

----------------------------------------------------------------------------- *)


        by rewrite /allocation_at /prev_job_nonpreemptive IDLE H_non_idling.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

From the preceding fact, we conclude that the generated schedule is indeed work-conserving.
    Theorem np_schedule_work_conserving:
      work_conserving arr_seq schedule.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 78)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  ============================
  work_conserving arr_seq schedule

----------------------------------------------------------------------------- *)


    Proof.
      movej t ARRIVES BACKLOGGED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 83)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged schedule j t
  ============================
  exists j_other : Job, scheduled_at schedule j_other t

----------------------------------------------------------------------------- *)


      move: (@ideal_proc_model_sched_case_analysis Job schedule t) ⇒ [IDLE|SCHED]; last by exact.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 97)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged schedule j t
  IDLE : is_idle schedule t
  ============================
  exists j_other : Job, scheduled_at schedule j_other t

----------------------------------------------------------------------------- *)


      exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 99)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged schedule j t
  IDLE : is_idle schedule t
  ============================
  False

----------------------------------------------------------------------------- *)


      have NON_EMPTY: j \in jobs_backlogged_at arr_seq schedule t by apply mem_backlogged_jobs ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 121)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged schedule j t
  IDLE : is_idle schedule t
  NON_EMPTY : j \in jobs_backlogged_at arr_seq schedule t
  ============================
  False

----------------------------------------------------------------------------- *)


      clear BACKLOGGED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 122)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  IDLE : is_idle schedule t
  NON_EMPTY : j \in jobs_backlogged_at arr_seq schedule t
  ============================
  False

----------------------------------------------------------------------------- *)


      move: (idle_schedule_no_backlogged_jobs t IDLE) ⇒ EMPTY.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 124)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_non_idling : forall (t : instant) (s : seq Job),
                 choose_job t s = idle_state <-> s = [::]
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  IDLE : is_idle schedule t
  NON_EMPTY : j \in jobs_backlogged_at arr_seq schedule t
  EMPTY : jobs_backlogged_at arr_seq schedule t = [::]
  ============================
  False

----------------------------------------------------------------------------- *)


      by rewrite EMPTY in NON_EMPTY.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

  End WorkConservation.

The next result establishes that the generated preemption-model-aware schedule is structurally valid, meaning all jobs stem from the arrival sequence and only ready jobs are scheduled.
  Section Validity.

Any reasonable job selection policy will not create jobs "out of thin air," i.e., if a job is selected, it was among those given to choose from.
    Hypothesis H_chooses_from_set:
       t s j, choose_job t s = Some j j \in s.

For the schedule to be valid, we require the notion of readiness to be consistent with the preemption model: a non-preemptive job remains ready until (at least) the end of its current non-preemptive section.
First, we show that if a job is chosen from the list of backlogged jobs, then it must be ready.
    Lemma choose_job_implies_job_ready:
       t j,
      choose_job t.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t) t.+1) = Some j
       job_ready schedule j t.+1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 73)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  ============================
  forall (t : nat) (j : Job),
  choose_job t.+1
    (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t) t.+1) =
  Some j -> job_ready schedule j t.+1

----------------------------------------------------------------------------- *)


    Proof.
      movet j IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 76)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  t : nat
  j : Job
  IN : choose_job t.+1
         (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t)
            t.+1) = Some j
  ============================
  job_ready schedule j t.+1

----------------------------------------------------------------------------- *)


      move: (H_chooses_from_set _ _ _ IN).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 83)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  t : nat
  j : Job
  IN : choose_job t.+1
         (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t)
            t.+1) = Some j
  ============================
  j \in jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t) t.+1 ->
  job_ready schedule j t.+1

----------------------------------------------------------------------------- *)


      rewrite mem_filter /backlogged ⇒ /andP [/andP [READY _] _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 178)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  t : nat
  j : Job
  IN : choose_job t.+1
         (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t)
            t.+1) = Some j
  READY : job_ready (schedule_up_to policy idle_state t) j t.+1
  ============================
  job_ready schedule j t.+1

----------------------------------------------------------------------------- *)


      rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t) schedule j t.+1) //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 186)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  t : nat
  j : Job
  IN : choose_job t.+1
         (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t)
            t.+1) = Some j
  READY : job_ready (schedule_up_to policy idle_state t) j t.+1
  ============================
  identical_prefix (schedule_up_to policy idle_state t) schedule t.+1

----------------------------------------------------------------------------- *)


      by apply schedule_up_to_identical_prefix.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

Next, we show that, under these natural assumptions, the generated schedule is valid.
    Theorem np_schedule_valid:
      valid_schedule schedule arr_seq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 81)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  ============================
  valid_schedule schedule arr_seq

----------------------------------------------------------------------------- *)


    Proof.
      split; movej t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 108)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t : instant
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t t == Some j ->
  arrives_in arr_seq j

subgoal 2 (ID 126) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t t == Some j ->
 job_ready
   (fun t0 : instant =>
    schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) j t

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t : instant
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t t == Some j ->
  arrives_in arr_seq j

----------------------------------------------------------------------------- *)


elim: t ⇒ [/eqP | t' IH /eqP].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 200)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None 0 0 = Some j ->
  arrives_in arr_seq j

subgoal 2 (ID 201) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j ->
 arrives_in arr_seq j

----------------------------------------------------------------------------- *)


        - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptiveIN.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 221)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  IN : choose_job 0 (jobs_backlogged_at arr_seq (empty_schedule None) 0) =
       Some j
  ============================
  arrives_in arr_seq j

subgoal 2 (ID 201) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j ->
 arrives_in arr_seq j

----------------------------------------------------------------------------- *)


          move: (H_chooses_from_set _ _ _ IN).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 228)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  IN : choose_job 0 (jobs_backlogged_at arr_seq (empty_schedule None) 0) =
       Some j
  ============================
  j \in jobs_backlogged_at arr_seq (empty_schedule None) 0 ->
  arrives_in arr_seq j

subgoal 2 (ID 201) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j ->
 arrives_in arr_seq j

----------------------------------------------------------------------------- *)


          by apply backlogged_job_arrives_in.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 201)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       arrives_in arr_seq j
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j ->
  arrives_in arr_seq j

----------------------------------------------------------------------------- *)


        - rewrite schedule_up_to_def /allocation_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 248)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       arrives_in arr_seq j
  ============================
  (if
    prev_job_nonpreemptive
      (schedule_up_to
         (fun (sched_prefix : schedule.schedule (processor_state Job))
            (t : instant) =>
          if prev_job_nonpreemptive sched_prefix t
          then sched_prefix t.-1
          else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None
         t') t'.+1
   then
    schedule_up_to
      (fun (sched_prefix : schedule.schedule (processor_state Job))
         (t : instant) =>
       if prev_job_nonpreemptive sched_prefix t
       then sched_prefix t.-1
       else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t'
      t'.+1.-1
   else
    choose_job t'.+1
      (jobs_backlogged_at arr_seq
         (schedule_up_to
            (fun (sched_prefix : schedule.schedule (processor_state Job))
               (t : instant) =>
             if prev_job_nonpreemptive sched_prefix t
             then sched_prefix t.-1
             else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
            None t') t'.+1)) = Some j -> arrives_in arr_seq j

----------------------------------------------------------------------------- *)


          case: (prev_job_nonpreemptive (schedule_up_to _ _ t') t'.+1) ⇒ [|IN];
                first by rewrite -pred_SnSCHED; apply IH; apply /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 263)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       arrives_in arr_seq j
  IN : choose_job t'.+1
         (jobs_backlogged_at arr_seq
            (schedule_up_to
               (fun (sched_prefix : schedule.schedule (processor_state Job))
                  (t : instant) =>
                if prev_job_nonpreemptive sched_prefix t
                then sched_prefix t.-1
                else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
               None t') t'.+1) = Some j
  ============================
  arrives_in arr_seq j

----------------------------------------------------------------------------- *)


          move: (H_chooses_from_set _ _ _ IN).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 303)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       arrives_in arr_seq j
  IN : choose_job t'.+1
         (jobs_backlogged_at arr_seq
            (schedule_up_to
               (fun (sched_prefix : schedule.schedule (processor_state Job))
                  (t : instant) =>
                if prev_job_nonpreemptive sched_prefix t
                then sched_prefix t.-1
                else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
               None t') t'.+1) = Some j
  ============================
  j
    \in jobs_backlogged_at arr_seq
          (schedule_up_to
             (fun (sched_prefix : schedule.schedule (processor_state Job))
                (t : instant) =>
              if prev_job_nonpreemptive sched_prefix t
              then sched_prefix t.-1
              else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
             None t') t'.+1 -> arrives_in arr_seq j

----------------------------------------------------------------------------- *)


          by apply backlogged_job_arrives_in.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 126) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t t == Some j ->
 job_ready
   (fun t0 : instant =>
    schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) j t

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 126)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t : instant
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t t == Some j ->
  job_ready
    (fun t0 : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) j t

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 126)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t : instant
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t t == Some j ->
  job_ready
    (fun t0 : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t0 t0) j t

----------------------------------------------------------------------------- *)


elim: t ⇒ [/eqP |t' IH /eqP].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 383)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None 0 0 = Some j ->
  job_ready
    (fun t : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t t) j 0

subgoal 2 (ID 384) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j ->
 job_ready
   (fun t : instant =>
    schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'.+1

----------------------------------------------------------------------------- *)


        - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptiveIN.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 404)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  IN : choose_job 0 (jobs_backlogged_at arr_seq (empty_schedule None) 0) =
       Some j
  ============================
  job_ready
    (fun t : instant =>
     schedule_up_to
       (fun (sched_prefix : schedule.schedule (processor_state Job))
          (t0 : instant) =>
        if
         match t0 with
         | 0 => false
         | t'.+1 =>
             match sched_prefix t' with
             | Some j0 => ~~ job_preemptable j0 (service sched_prefix j0 t0)
             | None => false
             end
         end
        then sched_prefix t0.-1
        else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None
       t t) j 0

subgoal 2 (ID 384) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j ->
 job_ready
   (fun t : instant =>
    schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'.+1

----------------------------------------------------------------------------- *)


          move: (H_chooses_from_set _ _ _ IN).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 411)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  IN : choose_job 0 (jobs_backlogged_at arr_seq (empty_schedule None) 0) =
       Some j
  ============================
  j \in jobs_backlogged_at arr_seq (empty_schedule None) 0 ->
  job_ready
    (fun t : instant =>
     schedule_up_to
       (fun (sched_prefix : schedule.schedule (processor_state Job))
          (t0 : instant) =>
        if
         match t0 with
         | 0 => false
         | t'.+1 =>
             match sched_prefix t' with
             | Some j0 => ~~ job_preemptable j0 (service sched_prefix j0 t0)
             | None => false
             end
         end
        then sched_prefix t0.-1
        else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None
       t t) j 0

subgoal 2 (ID 384) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j ->
 job_ready
   (fun t : instant =>
    schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'.+1

----------------------------------------------------------------------------- *)


          rewrite mem_filter /backlogged ⇒ /andP [/andP [READY _] _].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 506)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  IN : choose_job 0 (jobs_backlogged_at arr_seq (empty_schedule None) 0) =
       Some j
  READY : job_ready (empty_schedule None) j 0
  ============================
  job_ready
    (fun t : instant =>
     schedule_up_to
       (fun (sched_prefix : schedule.schedule (processor_state Job))
          (t0 : instant) =>
        if
         match t0 with
         | 0 => false
         | t'.+1 =>
             match sched_prefix t' with
             | Some j0 => ~~ job_preemptable j0 (service sched_prefix j0 t0)
             | None => false
             end
         end
        then sched_prefix t0.-1
        else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None
       t t) j 0

subgoal 2 (ID 384) is:
 schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j ->
 job_ready
   (fun t : instant =>
    schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'.+1

----------------------------------------------------------------------------- *)


          by rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 384)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j ->
  job_ready
    (fun t : instant =>
     schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'.+1

----------------------------------------------------------------------------- *)


        - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 557)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  ============================
  (if
    match
      schedule_up_to
        (fun (sched_prefix : schedule.schedule (processor_state Job))
           (t : instant) =>
         if
          match t with
          | 0 => false
          | t'0.+1 =>
              match sched_prefix t'0 with
              | Some j0 => ~~ job_preemptable j0 (service sched_prefix j0 t)
              | None => false
              end
          end
         then sched_prefix t.-1
         else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None
        t' t'
    with
    | Some j0 =>
        ~~
        job_preemptable j0
          (service
             (schedule_up_to
                (fun (sched_prefix : schedule.schedule (processor_state Job))
                   (t : instant) =>
                 if
                  match t with
                  | 0 => false
                  | t'0.+1 =>
                      match sched_prefix t'0 with
                      | Some j1 =>
                          ~~ job_preemptable j1 (service sched_prefix j1 t)
                      | None => false
                      end
                  end
                 then sched_prefix t.-1
                 else
                  choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
                None t') j0 t'.+1)
    | None => false
    end
   then
    schedule_up_to
      (fun (sched_prefix : schedule.schedule (processor_state Job))
         (t : instant) =>
       if
        match t with
        | 0 => false
        | t'0.+1 =>
            match sched_prefix t'0 with
            | Some j0 => ~~ job_preemptable j0 (service sched_prefix j0 t)
            | None => false
            end
        end
       then sched_prefix t.-1
       else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t'
      t'.+1.-1
   else
    choose_job t'.+1
      (jobs_backlogged_at arr_seq
         (schedule_up_to
            (fun (sched_prefix : schedule.schedule (processor_state Job))
               (t : instant) =>
             if
              match t with
              | 0 => false
              | t'0.+1 =>
                  match sched_prefix t'0 with
                  | Some j0 =>
                      ~~ job_preemptable j0 (service sched_prefix j0 t)
                  | None => false
                  end
              end
             then sched_prefix t.-1
             else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
            None t') t'.+1)) = Some j ->
  job_ready
    (fun t : instant =>
     schedule_up_to
       (fun (sched_prefix : schedule.schedule (processor_state Job))
          (t0 : instant) =>
        if
         match t0 with
         | 0 => false
         | t'0.+1 =>
             match sched_prefix t'0 with
             | Some j0 => ~~ job_preemptable j0 (service sched_prefix j0 t0)
             | None => false
             end
         end
        then sched_prefix t0.-1
        else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None
       t t) j t'.+1

----------------------------------------------------------------------------- *)


          case: (schedule_up_to _ _ t' t') ⇒ [j' | IN]; last by apply choose_job_implies_job_ready.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 571)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  j' : Job
  ============================
  (if
    ~~
    job_preemptable j'
      (service
         (schedule_up_to
            (fun (sched_prefix : schedule.schedule (processor_state Job))
               (t : instant) =>
             if
              match t with
              | 0 => false
              | t'0.+1 =>
                  match sched_prefix t'0 with
                  | Some j0 =>
                      ~~ job_preemptable j0 (service sched_prefix j0 t)
                  | None => false
                  end
              end
             then sched_prefix t.-1
             else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
            None t') j' t'.+1)
   then Some j'
   else
    choose_job t'.+1
      (jobs_backlogged_at arr_seq
         (schedule_up_to
            (fun (sched_prefix : schedule.schedule (processor_state Job))
               (t : instant) =>
             if
              match t with
              | 0 => false
              | t'0.+1 =>
                  match sched_prefix t'0 with
                  | Some j0 =>
                      ~~ job_preemptable j0 (service sched_prefix j0 t)
                  | None => false
                  end
              end
             then sched_prefix t.-1
             else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
            None t') t'.+1)) = Some j ->
  job_ready
    (fun t : instant =>
     schedule_up_to
       (fun (sched_prefix : schedule.schedule (processor_state Job))
          (t0 : instant) =>
        if
         match t0 with
         | 0 => false
         | t'0.+1 =>
             match sched_prefix t'0 with
             | Some j0 => ~~ job_preemptable j0 (service sched_prefix j0 t0)
             | None => false
             end
         end
        then sched_prefix t0.-1
        else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None
       t t) j t'.+1

----------------------------------------------------------------------------- *)


          destruct (~~ job_preemptable j' _) eqn:NP ⇒ [EQ|IN]; last by apply choose_job_implies_job_ready.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 590)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  j' : Job
  NP : ~~
       job_preemptable j'
         (service
            (schedule_up_to
               (fun (sched_prefix : schedule.schedule (processor_state Job))
                  (t : instant) =>
                if
                 match t with
                 | 0 => false
                 | t'.+1 =>
                     match sched_prefix t' with
                     | Some j =>
                         ~~ job_preemptable j (service sched_prefix j t)
                     | None => false
                     end
                 end
                then sched_prefix t.-1
                else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
               None t') j' t'.+1) = true
  EQ : Some j' = Some j
  ============================
  job_ready
    (fun t : instant =>
     schedule_up_to
       (fun (sched_prefix : schedule.schedule (processor_state Job))
          (t0 : instant) =>
        if
         match t0 with
         | 0 => false
         | t'0.+1 =>
             match sched_prefix t'0 with
             | Some j0 => ~~ job_preemptable j0 (service sched_prefix j0 t0)
             | None => false
             end
         end
        then sched_prefix t0.-1
        else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None
       t t) j t'.+1

----------------------------------------------------------------------------- *)


          apply H_valid_preemption_behavior.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 593)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  j' : Job
  NP : ~~
       job_preemptable j'
         (service
            (schedule_up_to
               (fun (sched_prefix : schedule.schedule (processor_state Job))
                  (t : instant) =>
                if
                 match t with
                 | 0 => false
                 | t'.+1 =>
                     match sched_prefix t' with
                     | Some j =>
                         ~~ job_preemptable j (service sched_prefix j t)
                     | None => false
                     end
                 end
                then sched_prefix t.-1
                else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
               None t') j' t'.+1) = true
  EQ : Some j' = Some j
  ============================
  ~~
  job_preemptable j
    (service
       (fun t : instant =>
        schedule_up_to
          (fun (sched_prefix : schedule.schedule (processor_state Job))
             (t0 : instant) =>
           if
            match t0 with
            | 0 => false
            | t'0.+1 =>
                match sched_prefix t'0 with
                | Some j0 =>
                    ~~ job_preemptable j0 (service sched_prefix j0 t0)
                | None => false
                end
            end
           then sched_prefix t0.-1
           else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
          None t t) j t'.+1)

----------------------------------------------------------------------------- *)


          injection EQ ⇒ <-.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 599)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  j' : Job
  NP : ~~
       job_preemptable j'
         (service
            (schedule_up_to
               (fun (sched_prefix : schedule.schedule (processor_state Job))
                  (t : instant) =>
                if
                 match t with
                 | 0 => false
                 | t'.+1 =>
                     match sched_prefix t' with
                     | Some j =>
                         ~~ job_preemptable j (service sched_prefix j t)
                     | None => false
                     end
                 end
                then sched_prefix t.-1
                else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
               None t') j' t'.+1) = true
  EQ : Some j' = Some j
  ============================
  ~~
  job_preemptable j'
    (service
       (fun t : instant =>
        schedule_up_to
          (fun (sched_prefix : schedule.schedule (processor_state Job))
             (t0 : instant) =>
           if
            match t0 with
            | 0 => false
            | t'0.+1 =>
                match sched_prefix t'0 with
                | Some j0 =>
                    ~~ job_preemptable j0 (service sched_prefix j0 t0)
                | None => false
                end
            end
           then sched_prefix t0.-1
           else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
          None t t) j' t'.+1)

----------------------------------------------------------------------------- *)


          move: NP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 601)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  j' : Job
  EQ : Some j' = Some j
  ============================
  ~~
  job_preemptable j'
    (service
       (schedule_up_to
          (fun (sched_prefix : schedule.schedule (processor_state Job))
             (t : instant) =>
           if
            match t with
            | 0 => false
            | t'0.+1 =>
                match sched_prefix t'0 with
                | Some j0 =>
                    ~~ job_preemptable j0 (service sched_prefix j0 t)
                | None => false
                end
            end
           then sched_prefix t.-1
           else choose_job t (jobs_backlogged_at arr_seq sched_prefix t))
          None t') j' t'.+1) = true ->
  ~~
  job_preemptable j'
    (service
       (fun t : instant =>
        schedule_up_to
          (fun (sched_prefix : schedule.schedule (processor_state Job))
             (t0 : instant) =>
           if
            match t0 with
            | 0 => false
            | t'0.+1 =>
                match sched_prefix t'0 with
                | Some j0 =>
                    ~~ job_preemptable j0 (service sched_prefix j0 t0)
                | None => false
                end
            end
           then sched_prefix t0.-1
           else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
          None t t) j' t'.+1)

----------------------------------------------------------------------------- *)


          have <-: (service (schedule_up_to policy idle_state t') j' t'.+1
                    = service (fun t : instantschedule_up_to policy idle_state t t) j' t'.+1) ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 611)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  j' : Job
  EQ : Some j' = Some j
  ============================
  service (schedule_up_to policy idle_state t') j' t'.+1 =
  service (fun t : instant => schedule_up_to policy idle_state t t) j' t'.+1

----------------------------------------------------------------------------- *)


          rewrite /service.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 645)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  j' : Job
  EQ : Some j' = Some j
  ============================
  service_during (schedule_up_to policy idle_state t') j' 0 t'.+1 =
  service_during (fun t : instant => schedule_up_to policy idle_state t t) j'
    0 t'.+1

----------------------------------------------------------------------------- *)


          apply equal_prefix_implies_same_service_duringt /andP [_ BOUND].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 689)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_chooses_from_set : forall (t : instant) (s : seq Job) (j : Job),
                       choose_job t s = Some j -> j \in s
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  j : Job
  t' : nat
  IH : schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j ->
       job_ready
         (fun t : instant =>
          schedule_up_to (allocation_at arr_seq choose_job) None t t) j t'
  j' : Job
  EQ : Some j' = Some j
  t : nat
  BOUND : t < t'.+1
  ============================
  schedule_up_to policy idle_state t' t =
  schedule_up_to policy idle_state t t

----------------------------------------------------------------------------- *)


          by rewrite (schedule_up_to_prefix_inclusion _ _ t t').
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

  End Validity.

Next, we observe that the resulting schedule is consistent with the definition of "preemption times".
  Section PreemptionTimes.

For notational convenience, recall the definition of a prefix of the schedule based on which the next decision is made.
    Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.

First, we observe that non-preemptive jobs remain scheduled as long as they are non-preemptive.
    Lemma np_job_remains_scheduled:
       t,
        prev_job_nonpreemptive (prefix t) t
        schedule_up_to policy idle_state t t = schedule_up_to policy idle_state t t.-1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 51)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  ============================
  forall t : nat,
  prev_job_nonpreemptive (prefix t) t ->
  schedule_up_to policy idle_state t t =
  schedule_up_to policy idle_state t t.-1

----------------------------------------------------------------------------- *)


    Proof.
      elim ⇒ [|t _] // NP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 90)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  NP : prev_job_nonpreemptive (prefix t.+1) t.+1
  ============================
  schedule_up_to policy idle_state t.+1 t.+1 =
  schedule_up_to policy idle_state t.+1 t.+1.-1

----------------------------------------------------------------------------- *)


      rewrite schedule_up_to_def /allocation_at /policy /allocation_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 112)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  NP : prev_job_nonpreemptive (prefix t.+1) t.+1
  ============================
  (if
    prev_job_nonpreemptive
      (schedule_up_to
         (fun (sched_prefix : schedule.schedule (processor_state Job))
            (t0 : instant) =>
          if prev_job_nonpreemptive sched_prefix t0
          then sched_prefix t0.-1
          else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
         idle_state t) t.+1
   then
    schedule_up_to
      (fun (sched_prefix : schedule.schedule (processor_state Job))
         (t0 : instant) =>
       if prev_job_nonpreemptive sched_prefix t0
       then sched_prefix t0.-1
       else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
      idle_state t t.+1.-1
   else
    choose_job t.+1
      (jobs_backlogged_at arr_seq
         (schedule_up_to
            (fun (sched_prefix : schedule.schedule (processor_state Job))
               (t0 : instant) =>
             if prev_job_nonpreemptive sched_prefix t0
             then sched_prefix t0.-1
             else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
            idle_state t) t.+1)) =
  schedule_up_to
    (fun (sched_prefix : schedule.schedule (processor_state Job))
       (t0 : instant) =>
     if prev_job_nonpreemptive sched_prefix t0
     then sched_prefix t0.-1
     else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
    idle_state t.+1 t.+1.-1

----------------------------------------------------------------------------- *)


      rewrite ifT // -pred_Sn.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 144)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  NP : prev_job_nonpreemptive (prefix t.+1) t.+1
  ============================
  schedule_up_to
    (fun (sched_prefix : schedule.schedule (processor_state Job))
       (t0 : instant) =>
     if prev_job_nonpreemptive sched_prefix t0
     then sched_prefix t0.-1
     else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
    idle_state t t =
  schedule_up_to
    (fun (sched_prefix : schedule.schedule (processor_state Job))
       (t0 : instant) =>
     if prev_job_nonpreemptive sched_prefix t0
     then sched_prefix t0.-1
     else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
    idle_state t.+1 t

----------------------------------------------------------------------------- *)


      by rewrite schedule_up_to_widen.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

From this, we conclude that the predicate used to determine whether the previously scheduled job is nonpreemptive in the computation of [np_uni_schedule] is consistent with the existing notion of a [preemption_time].
    Lemma np_consistent:
       t,
        prev_job_nonpreemptive (prefix t) t
        ~~ preemption_time schedule t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  ============================
  forall t : nat,
  prev_job_nonpreemptive (prefix t) t -> ~~ preemption_time schedule t

----------------------------------------------------------------------------- *)


    Proof.
      elim ⇒ [|t _]; first by rewrite /prev_job_nonpreemptive.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 70)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  ============================
  prev_job_nonpreemptive (prefix t.+1) t.+1 ->
  ~~ preemption_time schedule t.+1

----------------------------------------------------------------------------- *)


      rewrite /schedule /np_uni_schedule /generic_schedule /preemption_time
              schedule_up_to_def /prefix /allocation_atNP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 130)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  NP : prev_job_nonpreemptive (schedule_up_to policy idle_state t) t.+1
  ============================
  ~~
  match
    (if
      prev_job_nonpreemptive
        (schedule_up_to
           (fun (sched_prefix : schedule.schedule (processor_state Job))
              (t0 : instant) =>
            if prev_job_nonpreemptive sched_prefix t0
            then sched_prefix t0.-1
            else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
           None t) t.+1
     then
      schedule_up_to
        (fun (sched_prefix : schedule.schedule (processor_state Job))
           (t0 : instant) =>
         if prev_job_nonpreemptive sched_prefix t0
         then sched_prefix t0.-1
         else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
        None t t.+1.-1
     else
      choose_job t.+1
        (jobs_backlogged_at arr_seq
           (schedule_up_to
              (fun (sched_prefix : schedule.schedule (processor_state Job))
                 (t0 : instant) =>
               if prev_job_nonpreemptive sched_prefix t0
               then sched_prefix t0.-1
               else
                choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0))
              None t) t.+1))
  with
  | Some j =>
      job_preemptable j
        (service
           (fun t0 : instant =>
            schedule_up_to
              (fun (sched_prefix : schedule.schedule (processor_state Job))
                 (t1 : instant) =>
               if prev_job_nonpreemptive sched_prefix t1
               then sched_prefix t1.-1
               else
                choose_job t1 (jobs_backlogged_at arr_seq sched_prefix t1))
              None t0 t0) j t.+1)
  | None => true
  end

----------------------------------------------------------------------------- *)


      rewrite ifT // -pred_Sn.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 162)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  NP : prev_job_nonpreemptive (schedule_up_to policy idle_state t) t.+1
  ============================
  ~~
  match
    schedule_up_to
      (fun (sched_prefix : schedule.schedule (processor_state Job))
         (t0 : instant) =>
       if prev_job_nonpreemptive sched_prefix t0
       then sched_prefix t0.-1
       else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None
      t t
  with
  | Some j =>
      job_preemptable j
        (service
           (fun t0 : instant =>
            schedule_up_to
              (fun (sched_prefix : schedule.schedule (processor_state Job))
                 (t1 : instant) =>
               if prev_job_nonpreemptive sched_prefix t1
               then sched_prefix t1.-1
               else
                choose_job t1 (jobs_backlogged_at arr_seq sched_prefix t1))
              None t0 t0) j t.+1)
  | None => true
  end

----------------------------------------------------------------------------- *)


      move: NP; rewrite /prev_job_nonpreemptive.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 169)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  ============================
  match schedule_up_to policy idle_state t t with
  | Some j =>
      ~~
      job_preemptable j (service (schedule_up_to policy idle_state t) j t.+1)
  | None => false
  end ->
  ~~
  match
    schedule_up_to
      (fun (sched_prefix : schedule.schedule (processor_state Job))
         (t0 : instant) =>
       if
        match t0 with
        | 0 => false
        | t'.+1 =>
            match sched_prefix t' with
            | Some j => ~~ job_preemptable j (service sched_prefix j t0)
            | None => false
            end
        end
       then sched_prefix t0.-1
       else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None
      t t
  with
  | Some j =>
      job_preemptable j
        (service
           (fun t0 : instant =>
            schedule_up_to
              (fun (sched_prefix : schedule.schedule (processor_state Job))
                 (t1 : instant) =>
               if
                match t1 with
                | 0 => false
                | t'.+1 =>
                    match sched_prefix t' with
                    | Some j0 =>
                        ~~ job_preemptable j0 (service sched_prefix j0 t1)
                    | None => false
                    end
                end
               then sched_prefix t1.-1
               else
                choose_job t1 (jobs_backlogged_at arr_seq sched_prefix t1))
              None t0 t0) j t.+1)
  | None => true
  end

----------------------------------------------------------------------------- *)


      elim: (schedule_up_to policy idle_state t t) ⇒ // j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 206)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  j : Job
  ============================
  ~~ job_preemptable j (service (schedule_up_to policy idle_state t) j t.+1) ->
  ~~
  job_preemptable j
    (service
       (fun t0 : instant =>
        schedule_up_to
          (fun (sched_prefix : schedule.schedule (processor_state Job))
             (t1 : instant) =>
           if
            match t1 with
            | 0 => false
            | t'.+1 =>
                match sched_prefix t' with
                | Some j0 =>
                    ~~ job_preemptable j0 (service sched_prefix j0 t1)
                | None => false
                end
            end
           then sched_prefix t1.-1
           else choose_job t1 (jobs_backlogged_at arr_seq sched_prefix t1))
          None t0 t0) j t.+1)

----------------------------------------------------------------------------- *)


      have ->: (service (fun t0 : instantschedule_up_to policy idle_state t0 t0) j t.+1 =
                service (schedule_up_to policy idle_state t) j t.+1) ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 216)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  j : Job
  ============================
  service (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j t.+1 =
  service (schedule_up_to policy idle_state t) j t.+1

----------------------------------------------------------------------------- *)


      rewrite /service.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 250)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  j : Job
  ============================
  service_during (fun t0 : instant => schedule_up_to policy idle_state t0 t0)
    j 0 t.+1 = service_during (schedule_up_to policy idle_state t) j 0 t.+1

----------------------------------------------------------------------------- *)


      apply equal_prefix_implies_same_service_duringt' /andP [_ BOUND].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 294)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  t : nat
  j : Job
  t' : nat
  BOUND : t' < t.+1
  ============================
  schedule_up_to policy idle_state t' t' =
  schedule_up_to policy idle_state t t'

----------------------------------------------------------------------------- *)


      by rewrite (schedule_up_to_prefix_inclusion _ _ t' t).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

  End PreemptionTimes.

Finally, we establish the main feature: the generated schedule respects the preemption-model semantics.
  Section PreemptionCompliance.

As a minimal validity requirement (which is a part of [valid_preemption_model]), we require that any job in [arr_seq] must start execution to become nonpreemptive.
    Hypothesis H_valid_preemption_function :
       j,
        arrives_in arr_seq j
        job_cannot_become_nonpreemptive_before_execution j.

Given such a valid preemption model, we establish that the generated schedule indeed respects the preemption model semantics.
    Lemma np_respects_preemption_model :
      schedule_respects_preemption_model arr_seq schedule.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 47)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  ============================
  schedule_respects_preemption_model arr_seq schedule

----------------------------------------------------------------------------- *)


    Proof.
      movej.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 49)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  ============================
  forall t : instant,
  arrives_in arr_seq j ->
  ~~ job_preemptable j (service schedule j t) -> scheduled_at schedule j t

----------------------------------------------------------------------------- *)


      elim ⇒ [| t' IH]; first by rewrite service0ARR /negP NP; move: (H_valid_preemption_function j ARR).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 61)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ============================
  arrives_in arr_seq j ->
  ~~ job_preemptable j (service schedule j t'.+1) ->
  scheduled_at schedule j t'.+1

----------------------------------------------------------------------------- *)


      moveARR NP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 121)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NP : ~~ job_preemptable j (service schedule j t'.+1)
  ============================
  scheduled_at schedule j t'.+1

----------------------------------------------------------------------------- *)


      have: scheduled_at schedule j t'.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 125)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NP : ~~ job_preemptable j (service schedule j t'.+1)
  ============================
  scheduled_at schedule j t'

subgoal 2 (ID 126) is:
 scheduled_at schedule j t' -> scheduled_at schedule j t'.+1

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 125)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NP : ~~ job_preemptable j (service schedule j t'.+1)
  ============================
  scheduled_at schedule j t'

----------------------------------------------------------------------------- *)


apply contraTNOT_SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 128)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NP : ~~ job_preemptable j (service schedule j t'.+1)
  NOT_SCHED : ~~ scheduled_at schedule j t'
  ============================
  false

----------------------------------------------------------------------------- *)


        move: (not_scheduled_implies_no_service _ _ _ NOT_SCHED) ⇒ NO_SERVICE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 139)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NP : ~~ job_preemptable j (service schedule j t'.+1)
  NOT_SCHED : ~~ scheduled_at schedule j t'
  NO_SERVICE : service_at schedule j t' = 0
  ============================
  false

----------------------------------------------------------------------------- *)


        rewrite -(service_last_plus_before) NO_SERVICE addn0 in NP; apply IH in NP ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 187)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NOT_SCHED : ~~ scheduled_at schedule j t'
  NO_SERVICE : service_at schedule j t' = 0
  NP : scheduled_at schedule j t'
  ============================
  false

----------------------------------------------------------------------------- *)


        by move /negP in NOT_SCHED.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 126) is:
 scheduled_at schedule j t' -> scheduled_at schedule j t'.+1

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 126)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NP : ~~ job_preemptable j (service schedule j t'.+1)
  ============================
  scheduled_at schedule j t' -> scheduled_at schedule j t'.+1

----------------------------------------------------------------------------- *)


      rewrite !scheduled_at_def /schedule/np_uni_schedule/generic_schedule ⇒ /eqP SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 342)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NP : ~~ job_preemptable j (service schedule j t'.+1)
  SCHED : schedule_up_to (allocation_at arr_seq choose_job) None t' t' =
          Some j
  ============================
  schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 ==
  Some j

----------------------------------------------------------------------------- *)


      rewrite -SCHED (schedule_up_to_prefix_inclusion _ _ t' t'.+1) // np_job_remains_scheduled //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 387)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NP : ~~ job_preemptable j (service schedule j t'.+1)
  SCHED : schedule_up_to (allocation_at arr_seq choose_job) None t' t' =
          Some j
  ============================
  prev_job_nonpreemptive (schedule_up_to policy idle_state t') t'.+1

----------------------------------------------------------------------------- *)


      rewrite /prev_job_nonpreemptive SCHED (identical_prefix_service _ schedule) //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 431)
  
  Job : JobType
  JC : JobCost Job
  JA : JobArrival Job
  PState := processor_state Job : Type
  idle_state := None : PState
  arr_seq : arrival_sequence Job
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  RM : JobReady Job (processor_state Job)
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  H : JobPreemptable Job
  choose_job : instant -> seq Job -> option Job
  schedule := np_uni_schedule arr_seq choose_job
   : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_job
   : schedule.schedule (processor_state Job) -> instant -> option Job
  H_valid_preemption_function : forall j : Job,
                                arrives_in arr_seq j ->
                                job_cannot_become_nonpreemptive_before_execution
                                  j
  j : Job
  t' : nat
  IH : arrives_in arr_seq j ->
       ~~ job_preemptable j (service schedule j t') ->
       scheduled_at schedule j t'
  ARR : arrives_in arr_seq j
  NP : ~~ job_preemptable j (service schedule j t'.+1)
  SCHED : schedule_up_to (allocation_at arr_seq choose_job) None t' t' =
          Some j
  ============================
  identical_prefix (schedule_up_to policy idle_state t') schedule t'.+1

----------------------------------------------------------------------------- *)


      by apply schedule_up_to_identical_prefix.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

  End PreemptionCompliance.

End NPUniprocessorScheduler.