Library prosa.implementation.facts.ideal_uni.prio_aware


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

Welcome to Coq 8.13.0 (January 2021)

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

Require Export prosa.implementation.facts.ideal_uni.preemption_aware.

Ideal Uniprocessor Scheduler Properties

This file establishes facts about the reference model of a priority- and preemption-model-aware ideal uniprocessor scheduler.
The following results assume ideal uniprocessor schedules.
Require Import prosa.model.processor.ideal.

Section PrioAwareUniprocessorScheduler.

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.
  Let PState := ideal.processor_state Job.
  Let idle_state : PState := None.

Suppose we are given a consistent arrival sequence of such jobs, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.

... a non-clairvoyant readiness model, ...
  Context {RM: JobReady Job (ideal.processor_state Job)}.
  Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.

... a preemption model that is consistent with the readiness model, ...
  Context `{JobPreemptable Job}.
  Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM.

... and reflexive, total, and transitive JLDP priority policy.
  Context `{JLDP_policy Job}.
  Hypothesis H_reflexive_priorities: reflexive_priorities.
  Hypothesis H_total: total_priorities.
  Hypothesis H_transitive: transitive_priorities.

Consider the schedule generated by the preemption-policy- and priority-aware ideal uniprocessor scheduler.
  Let schedule := uni_schedule arr_seq.

First, we note that the priority-aware job selection policy obviously maintains work-conservation.
  Corollary uni_schedule_work_conserving:
    work_conserving arr_seq schedule.

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

1 subgoal (ID 53)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  ============================
  work_conserving arr_seq schedule

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

  Proof.
    apply np_schedule_work_conserving ⇒ //.

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

1 subgoal (ID 59)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  ============================
  forall (t : instant) (s : seq Job),
  choose_highest_prio_job t s = None <-> s = [::]

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

    move⇒ t jobs.

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

1 subgoal (ID 149)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  t : instant
  jobs : seq Job
  ============================
  choose_highest_prio_job t jobs = None <-> jobs = [::]

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

    rewrite /choose_highest_prio_job; split.

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

2 subgoals (ID 156)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  t : instant
  jobs : seq Job
  ============================
  supremum (hep_job_at t) jobs = None -> jobs = [::]

subgoal 2 (ID 157) is:
 jobs = [::] -> supremum (hep_job_at t) jobs = None

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

    - by apply supremum_none.

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

1 subgoal (ID 157)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  t : instant
  jobs : seq Job
  ============================
  jobs = [::] -> supremum (hep_job_at t) jobs = None

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

    - by move⇒ →.

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

No more subgoals.

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

  Qed.

Second, we similarly note that schedule validity is also maintained.
  Corollary uni_schedule_valid:
    valid_schedule schedule arr_seq.

(* ----------------------------------[ 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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  ============================
  valid_schedule schedule arr_seq

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

  Proof.
    apply np_schedule_valid ⇒ //.

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

1 subgoal (ID 66)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  ============================
  forall (t : instant) (s : seq Job) (j : Job),
  choose_highest_prio_job t s = Some j -> j \in s

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

    move⇒ t jobs j.

(* ----------------------------------[ 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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  t : instant
  jobs : seq Job
  j : Job
  ============================
  choose_highest_prio_job t jobs = Some j -> j \in jobs

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

    now apply supremum_in.

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

No more subgoals.

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

  Qed.

Third, the schedule respects also the preemption model semantics.
  Section PreemptionCompliance.

Suppose that every job in [arr_seq] adheres to the basic validity requirement that jobs must start execution to become nonpreemptive.
    Hypothesis H_valid_preemption_function :
      ∀ j,
        arrives_in arr_seq j →
        job_cannot_become_nonpreemptive_before_execution j.

Since [uni_schedule arr_seq] is an instance of [np_uni_schedule], the compliance of [schedule] with the preemption model follows trivially from the compliance of [np_uni_schedule].
    Corollary schedule_respects_preemption_model :
      schedule_respects_preemption_model arr_seq schedule.

(* ----------------------------------[ 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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state 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.
      by apply np_respects_preemption_model.

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

No more subgoals.

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

    Qed.

  End PreemptionCompliance.

Now we proceed to the main property of the priority-aware scheduler: in the following section we establish that [uni_schedule arr_seq] is compliant with the given priority policy whenever jobs are preemptable.
  Section Priority.

For notational convenience, recall the definitions of the job-selection policy and a prefix of the schedule based on which the next decision is made.
    Let policy := allocation_at arr_seq choose_highest_prio_job.
    Let prefix t := if t is t'.+1
                    then schedule_up_to policy idle_state t'
                    else empty_schedule idle_state.

To start, we observe that, at preemption times, the scheduled job is a supremum w.r.t. to the priority order and the set of backlogged jobs.
    Lemma scheduled_job_is_supremum:
      ∀ j t,
        scheduled_at schedule j t →
        preemption_time schedule t →
        supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j.

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

1 subgoal (ID 94)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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 (j : Job) (t : instant),
  scheduled_at schedule j t ->
  preemption_time schedule t ->
  supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j

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

    Proof.
      move⇒ j t SCHED PREEMPT.

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

1 subgoal (ID 98)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j : Job
  t : instant
  SCHED : scheduled_at schedule j t
  PREEMPT : preemption_time schedule t
  ============================
  supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j

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

      have NOT_NP: ~~ prev_job_nonpreemptive (prefix t) t.

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

2 subgoals (ID 101)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j : Job
  t : instant
  SCHED : scheduled_at schedule j t
  PREEMPT : preemption_time schedule t
  ============================
  ~~ prev_job_nonpreemptive (prefix t) t

subgoal 2 (ID 103) is:
 supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j

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

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

1 subgoal (ID 101)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j : Job
  t : instant
  SCHED : scheduled_at schedule j t
  PREEMPT : preemption_time schedule t
  ============================
  ~~ prev_job_nonpreemptive (prefix t) t

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

apply contraL with (b := preemption_time (uni_schedule arr_seq) t) ⇒ //.

(* ----------------------------------[ 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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j : Job
  t : instant
  SCHED : scheduled_at schedule j t
  PREEMPT : preemption_time schedule t
  ============================
  prev_job_nonpreemptive (prefix t) t ->
  ~~ preemption_time (uni_schedule arr_seq) t

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

        now apply np_consistent.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 103) is:
 supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j

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

}

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

1 subgoal (ID 103)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j : Job
  t : instant
  SCHED : scheduled_at schedule j t
  PREEMPT : preemption_time schedule t
  NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
  ============================
  supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j

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

      move: SCHED.

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

1 subgoal (ID 141)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j : Job
  t : instant
  PREEMPT : preemption_time schedule t
  NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
  ============================
  scheduled_at schedule j t ->
  supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j

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

      rewrite scheduled_at_def ⇒ /eqP.

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

1 subgoal (ID 180)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j : Job
  t : instant
  PREEMPT : preemption_time schedule t
  NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
  ============================
  schedule t = Some j ->
  supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j

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

      rewrite {1}/schedule/uni_schedule/np_uni_schedule/generic_schedule schedule_up_to_def /allocation_at -/(prefix t).

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

1 subgoal (ID 213)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j : Job
  t : instant
  PREEMPT : preemption_time schedule t
  NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
  ============================
  (if prev_job_nonpreemptive (prefix t) t
   then prefix t t.-1
   else choose_highest_prio_job t (jobs_backlogged_at arr_seq (prefix t) t)) =
  Some j ->
  supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j

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

      rewrite ifF //.

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

1 subgoal (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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j : Job
  t : instant
  PREEMPT : preemption_time schedule t
  NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
  ============================
  prev_job_nonpreemptive (prefix t) t = false

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

      now apply negbTE.

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

No more subgoals.

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

    Qed.

From the preceding facts, we conclude that [uni_schedule arr_seq] respects the priority policy at preemption times.
    Theorem schedule_respects_policy :
      respects_policy_at_preemption_point arr_seq schedule.

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

1 subgoal (ID 102)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  ============================
  respects_policy_at_preemption_point arr_seq schedule

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

    Proof.
      move⇒ j1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.

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

1 subgoal (ID 110)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  BACK_j1 : backlogged schedule j1 t
  SCHED_j2 : scheduled_at schedule j2 t
  ============================
  hep_job_at t j2 j1

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

      case: (boolP (scheduled_at (uni_schedule arr_seq) j1 t)) ⇒ [SCHED_j1|NOT_SCHED_j1].

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

2 subgoals (ID 172)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  BACK_j1 : backlogged schedule j1 t
  SCHED_j2 : scheduled_at schedule j2 t
  SCHED_j1 : scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  hep_job_at t j2 j1

subgoal 2 (ID 173) is:
 hep_job_at t j2 j1

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

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

1 subgoal (ID 172)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  BACK_j1 : backlogged schedule j1 t
  SCHED_j2 : scheduled_at schedule j2 t
  SCHED_j1 : scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  hep_job_at t j2 j1

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

have <-: j1 = j2 by apply (ideal_proc_model_is_a_uniprocessor_model j1 j2 (uni_schedule arr_seq) t).

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

1 subgoal (ID 189)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  BACK_j1 : backlogged schedule j1 t
  SCHED_j2 : scheduled_at schedule j2 t
  SCHED_j1 : scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  hep_job_at t j1 j1

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

        now apply H_reflexive_priorities.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 173) is:
 hep_job_at t j2 j1

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

}

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

1 subgoal (ID 173)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  BACK_j1 : backlogged schedule j1 t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  hep_job_at t j2 j1

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

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

1 subgoal (ID 173)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  BACK_j1 : backlogged schedule j1 t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  hep_job_at t j2 j1

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

move: BACK_j1.

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

1 subgoal (ID 191)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  backlogged schedule j1 t -> hep_job_at t j2 j1

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

        have ->: backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t.

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

2 subgoals (ID 211)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t

subgoal 2 (ID 216) is:
 backlogged (prefix t) j1 t -> hep_job_at t j2 j1

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

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

1 subgoal (ID 211)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t

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

apply backlogged_prefix_invariance' with (h := t) ⇒ //.

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

2 subgoals (ID 224)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  identical_prefix (uni_schedule arr_seq) (prefix t) t

subgoal 2 (ID 226) is:
 ~~ scheduled_at (prefix t) j1 t

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

          rewrite /identical_prefix /uni_schedule /prefix ⇒ t' LT.

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

2 subgoals (ID 284)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  t' : nat
  LT : t' < t
  ============================
  np_uni_schedule arr_seq choose_highest_prio_job t' =
  match t with
  | 0 => empty_schedule idle_state
  | t'0.+1 => schedule_up_to policy idle_state t'0
  end t'

subgoal 2 (ID 226) is:
 ~~ scheduled_at (prefix t) j1 t

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

          induction t ⇒ //.

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

2 subgoals (ID 316)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : nat
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t.+1
  SCHED_j2 : scheduled_at schedule j2 t.+1
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t.+1
  t' : nat
  LT : t' < t.+1
  IHt : preemption_time schedule t ->
        scheduled_at schedule j2 t ->
        ~~ scheduled_at (uni_schedule arr_seq) j1 t ->
        t' < t ->
        np_uni_schedule arr_seq choose_highest_prio_job t' =
        match t with
        | 0 => empty_schedule idle_state
        | t'.+1 => schedule_up_to policy idle_state t'
        end t'
  ============================
  np_uni_schedule arr_seq choose_highest_prio_job t' =
  schedule_up_to policy idle_state t t'

subgoal 2 (ID 226) is:
 ~~ scheduled_at (prefix t) j1 t

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

          rewrite /np_uni_schedule /generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //.

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

1 subgoal (ID 226)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  ~~ scheduled_at (prefix t) j1 t

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

          rewrite /prefix scheduled_at_def.

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

1 subgoal (ID 393)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  match t with
  | 0 => empty_schedule idle_state
  | t'.+1 => schedule_up_to policy idle_state t'
  end t != Some j1

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

          induction t ⇒ //.

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

1 subgoal (ID 417)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : nat
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t.+1
  SCHED_j2 : scheduled_at schedule j2 t.+1
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t.+1
  IHt : preemption_time schedule t ->
        scheduled_at schedule j2 t ->
        ~~ scheduled_at (uni_schedule arr_seq) j1 t ->
        match t with
        | 0 => empty_schedule idle_state
        | t'.+1 => schedule_up_to policy idle_state t'
        end t != Some j1
  ============================
  schedule_up_to policy idle_state t t.+1 != Some j1

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

          now rewrite schedule_up_to_empty.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 216) is:
 backlogged (prefix t) j1 t -> hep_job_at t j2 j1

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

}

(* ----------------------------------[ 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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  ============================
  backlogged (prefix t) j1 t -> hep_job_at t j2 j1

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

        move⇒ BACK_j1.

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

1 subgoal (ID 449)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  BACK_j1 : backlogged (prefix t) j1 t
  ============================
  hep_job_at t j2 j1

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

        move: (scheduled_job_is_supremum j2 t SCHED_j2 PREEMPT) ⇒ SUPREMUM.

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

1 subgoal (ID 451)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  BACK_j1 : backlogged (prefix t) j1 t
  SUPREMUM : supremum (hep_job_at t)
               (jobs_backlogged_at arr_seq (prefix t) t) = 
             Some j2
  ============================
  hep_job_at t j2 j1

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

        apply supremum_spec with (s := jobs_backlogged_at arr_seq (prefix t) t) ⇒ //.

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

1 subgoal (ID 463)
  
  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
  H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
  H0 : JLDP_policy Job
  H_reflexive_priorities : reflexive_priorities
  H_total : total_priorities
  H_transitive : transitive_priorities
  schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
  policy := allocation_at arr_seq choose_highest_prio_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
  j1, j2 : Job
  t : instant
  ARRIVES : arrives_in arr_seq j1
  PREEMPT : preemption_time schedule t
  SCHED_j2 : scheduled_at schedule j2 t
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 t
  BACK_j1 : backlogged (prefix t) j1 t
  SUPREMUM : supremum (hep_job_at t)
               (jobs_backlogged_at arr_seq (prefix t) t) = 
             Some j2
  ============================
  j1 \in jobs_backlogged_at arr_seq (prefix t) t

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

        now apply mem_backlogged_jobs.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

    Qed.

  End Priority.

End PrioAwareUniprocessorScheduler.