Library prosa.implementation.facts.ideal_uni.prio_aware


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

Welcome to Coq 8.11.2 (June 2020)

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


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.
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, ...
... a preemption model that is consistent with the readiness model, ...
... 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.
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 363)
  
  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 369)
  
  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 = [::]

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


    movet jobs.

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

1 subgoal (ID 460)
  
  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 467)
  
  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 468) is:
 jobs = [::] -> supremum (hep_job_at t) jobs = None

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


    - by apply supremum_none.

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

1 subgoal (ID 468)
  
  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 371)
  
  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 376)
  
  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

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


    movet jobs j.

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

1 subgoal (ID 410)
  
  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.

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.
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 405)
  
  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
            | succn t' => 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.
      movej t SCHED PREEMPT.

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

1 subgoal (ID 409)
  
  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
            | succn t' => 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 412)
  
  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
            | succn t' => 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 414) is:
 supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j

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


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

1 subgoal (ID 412)
  
  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
            | succn t' => 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 423)
  
  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
            | succn t' => 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 (ID 414)

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

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


}

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

1 subgoal (ID 414)
  
  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
            | succn t' => 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 453)
  
  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
            | succn t' => 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 493)
  
  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
            | succn t' => 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 526)
  
  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
            | succn t' => 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 (predn t)
   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 534)
  
  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
            | succn t' => 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 413)
  
  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
            | succn t' => schedule_up_to policy idle_state t'
            end : nat -> schedule.schedule PState
  ============================
  respects_policy_at_preemption_point arr_seq schedule

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


    Proof.
      movej1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.

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

1 subgoal (ID 421)
  
  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
            | succn t' => 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 483)
  
  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
            | succn t' => 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 484) is:
 hep_job_at t j2 j1

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


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

1 subgoal (ID 483)
  
  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
            | succn t' => 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 501)
  
  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
            | succn t' => 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 (ID 484)

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

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


}

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

1 subgoal (ID 484)
  
  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
            | succn t' => 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 484)
  
  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
            | succn t' => 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 503)
  
  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
            | succn t' => 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 524)
  
  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
            | succn t' => 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 529) is:
 backlogged (prefix t) j1 t -> hep_job_at t j2 j1

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


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

1 subgoal (ID 524)
  
  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
            | succn t' => 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 537)
  
  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
            | succn t' => 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 539) is:
 ~~ scheduled_at (prefix t) j1 t

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


          rewrite /identical_prefix /uni_schedule /prefixt' LT.

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

2 subgoals (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
  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
            | succn t' => 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
  | succn t'0 => schedule_up_to policy idle_state t'0
  end t'

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

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


          induction t ⇒ //.

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

2 subgoals (ID 631)
  
  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
            | succn t' => 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 (succn t)
  SCHED_j2 : scheduled_at schedule j2 (succn t)
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 (succn t)
  t' : nat
  LT : t' < succn t
  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
        | succn t' => 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 539) is:
 ~~ scheduled_at (prefix t) j1 t

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


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

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

1 subgoal (ID 539)
  
  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
            | succn t' => 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 710)
  
  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
            | succn t' => 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
  | succn t' => schedule_up_to policy idle_state t'
  end t != Some j1

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


          induction t ⇒ //.

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

1 subgoal (ID 734)
  
  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
            | succn t' => 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 (succn t)
  SCHED_j2 : scheduled_at schedule j2 (succn t)
  NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 (succn t)
  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
        | succn t' => schedule_up_to policy idle_state t'
        end t != Some j1
  ============================
  schedule_up_to policy idle_state t (succn t) != Some j1

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


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

1 subgoal (ID 529)

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

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


}

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

1 subgoal (ID 529)
  
  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
            | succn t' => 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

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


        moveBACK_j1.

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

1 subgoal (ID 767)
  
  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
            | succn t' => 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 769)
  
  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
            | succn t' => 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 781)
  
  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
            | succn t' => 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.