Library prosa.analysis.facts.readiness.backlogged


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

Welcome to Coq 8.11.2 (June 2020)

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

Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.facts.behavior.arrivals.
Require Export prosa.analysis.definitions.readiness.

In this file, we establish basic facts about backlogged jobs.

Section BackloggedJobs.

Consider any kind of jobs with arrival times and costs...
  Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.

... and any kind of processor model, ...
  Context {PState : Type} `{ProcessorState Job PState}.

... and allow for any notion of job readiness.
  Context `{JobReady Job PState}.

Given an arrival sequence and a schedule ...
  Variable arr_seq : arrival_sequence Job.
  Variable sched : schedule PState.

... with consistent arrival times, ...
  Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.

... we observe that any backlogged job is indeed in the set of backlogged jobs.
  Lemma mem_backlogged_jobs:
    ∀ j t,
      arrives_in arr_seq j →
      backlogged sched j t →
      j \in jobs_backlogged_at arr_seq sched t.

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

1 subgoal (ID 652)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  ============================
  forall (j : Job) (t : instant),
  arrives_in arr_seq j ->
  backlogged sched j t -> j \in jobs_backlogged_at arr_seq sched t

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

  Proof.
    move⇒ j t ARRIVES BACKLOGGED.

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

1 subgoal (ID 656)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged sched j t
  ============================
  j \in jobs_backlogged_at arr_seq sched t

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

    rewrite /jobs_backlogged_at /arrivals_up_to.

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

1 subgoal (ID 672)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged sched j t
  ============================
  j
    \in [seq j0 <- arrivals_between arr_seq 0 (succn t)
           | backlogged sched j0 t]

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

    rewrite mem_filter.

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

1 subgoal (ID 678)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged sched j t
  ============================
  backlogged sched j t && (j \in arrivals_between arr_seq 0 (succn t))

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

    apply /andP; split; first by exact.

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

1 subgoal (ID 705)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged sched j t
  ============================
  j \in arrivals_between arr_seq 0 (succn t)

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

    apply arrived_between_implies_in_arrivals ⇒ //.

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

1 subgoal (ID 710)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged sched j t
  ============================
  arrived_between j 0 (succn t)

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

    rewrite /arrived_between.

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

1 subgoal (ID 737)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged sched j t
  ============================
  0 <= job_arrival j < succn t

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

    apply /andP; split ⇒ //.

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

1 subgoal (ID 764)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged sched j t
  ============================
  job_arrival j < succn t

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

    rewrite ltnS -/(has_arrived _ _).

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

1 subgoal (ID 803)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ARRIVES : arrives_in arr_seq j
  BACKLOGGED : backlogged sched j t
  ============================
  has_arrived j t

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

    now apply (backlogged_implies_arrived sched).

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

No more subgoals.

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

  Qed.

Trivially, it is also the case that any backlogged job comes from the respective arrival sequence.
  Lemma backlogged_job_arrives_in:
    ∀ j t,
      j \in jobs_backlogged_at arr_seq sched t →
      arrives_in arr_seq j.

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

1 subgoal (ID 667)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  ============================
  forall (j : Job) (t : instant),
  j \in jobs_backlogged_at arr_seq sched t -> arrives_in arr_seq j

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

  Proof.
    move⇒ j t.

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

1 subgoal (ID 669)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ============================
  j \in jobs_backlogged_at arr_seq sched t -> arrives_in arr_seq j

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

    rewrite /jobs_backlogged_at mem_filter ⇒ /andP [_ IN].

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

1 subgoal (ID 728)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  IN : j \in arrivals_up_to arr_seq t
  ============================
  arrives_in arr_seq j

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

    move: IN.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 730)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ============================
  j \in arrivals_up_to arr_seq t -> arrives_in arr_seq j

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

rewrite /arrivals_up_to.

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

1 subgoal (ID 733)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1, H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_consistent_arrival_times : consistent_arrival_times arr_seq
  j : Job
  t : instant
  ============================
  j \in arrivals_between arr_seq 0 (succn t) -> arrives_in arr_seq j

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

    now apply in_arrivals_implies_arrived.

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

No more subgoals.

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

  Qed.

End BackloggedJobs.

In the following section, we make one more crucial assumption: namely, that the readiness model is non-clairvoyant, which allows us to relate backlogged jobs in schedules with a shared prefix.
Section NonClairvoyance.

Consider any kind of jobs with arrival times and costs...
  Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.

... any kind of processor model, ...
  Context {PState : Type} `{ProcessorState Job PState}.

... and allow for any non-clairvoyant notion of job readiness.
  Context {RM : JobReady Job PState}.
  Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.

Consider any arrival sequence ...
  Variable arr_seq : arrival_sequence Job.

... and two schedules ...
  Variable sched sched': schedule PState.

... with a shared prefix to a fixed horizon.
  Variable h : instant.
  Hypothesis H_shared_prefix: identical_prefix sched sched' h.

We observe that a job is backlogged at a time in the prefix in one schedule iff it is backlogged in the other schedule due to the non-clairvoyance of the notion of job readiness ...
  Lemma backlogged_prefix_invariance:
    ∀ t j,
      t < h →
      backlogged sched j t = backlogged sched' j t.

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

1 subgoal (ID 655)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  ============================
  forall (t : nat) (j : Job),
  t < h -> backlogged sched j t = backlogged sched' j t

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

  Proof.
    move⇒ t j IN_PREFIX.

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

1 subgoal (ID 658)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : nat
  j : Job
  IN_PREFIX : t < h
  ============================
  backlogged sched j t = backlogged sched' j t

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

    rewrite /backlogged.

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

1 subgoal (ID 671)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : nat
  j : Job
  IN_PREFIX : t < h
  ============================
  job_ready sched j t && ~~ scheduled_at sched j t =
  job_ready sched' j t && ~~ scheduled_at sched' j t

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

    rewrite (H_nonclairvoyant_job_readiness sched sched' j h) //.

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

2 subgoals (ID 676)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : nat
  j : Job
  IN_PREFIX : t < h
  ============================
  job_ready sched' j t && ~~ scheduled_at sched j t =
  job_ready sched' j t && ~~ scheduled_at sched' j t

subgoal 2 (ID 678) is:
 t <= h

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

    rewrite /scheduled_at H_shared_prefix //.

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

1 subgoal (ID 678)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : nat
  j : Job
  IN_PREFIX : t < h
  ============================
  t <= h

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

    now apply ltnW.

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

No more subgoals.

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

  Qed.

As a corollary, if we further know that j is not scheduled at time [h], we can expand the previous lemma to [t <= h].
  Corollary backlogged_prefix_invariance':
    ∀ t j,
      ~~ scheduled_at sched j t →
      ~~ scheduled_at sched' j t →
      t ≤ h →
      backlogged sched j t = backlogged sched' j t.

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

1 subgoal (ID 682)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  ============================
  forall (t : instant) (j : Job),
  ~~ scheduled_at sched j t ->
  ~~ scheduled_at sched' j t ->
  t <= h -> backlogged sched j t = backlogged sched' j t

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

  Proof.
    move⇒ t j NOT_SCHED NOT_SCHED'.

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

1 subgoal (ID 686)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : instant
  j : Job
  NOT_SCHED : ~~ scheduled_at sched j t
  NOT_SCHED' : ~~ scheduled_at sched' j t
  ============================
  t <= h -> backlogged sched j t = backlogged sched' j t

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

    rewrite leq_eqVlt ⇒ /orP [/eqP EQ | LT]; last by apply backlogged_prefix_invariance.

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

1 subgoal (ID 765)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : instant
  j : Job
  NOT_SCHED : ~~ scheduled_at sched j t
  NOT_SCHED' : ~~ scheduled_at sched' j t
  EQ : t = h
  ============================
  backlogged sched j t = backlogged sched' j t

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

    rewrite /backlogged.

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

1 subgoal (ID 780)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : instant
  j : Job
  NOT_SCHED : ~~ scheduled_at sched j t
  NOT_SCHED' : ~~ scheduled_at sched' j t
  EQ : t = h
  ============================
  job_ready sched j t && ~~ scheduled_at sched j t =
  job_ready sched' j t && ~~ scheduled_at sched' j t

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

    rewrite (H_nonclairvoyant_job_readiness sched sched' j h) //;
            last by rewrite EQ.

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

1 subgoal (ID 785)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : instant
  j : Job
  NOT_SCHED : ~~ scheduled_at sched j t
  NOT_SCHED' : ~~ scheduled_at sched' j t
  EQ : t = h
  ============================
  job_ready sched' j t && ~~ scheduled_at sched j t =
  job_ready sched' j t && ~~ scheduled_at sched' j t

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

    now rewrite NOT_SCHED NOT_SCHED'.

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

No more subgoals.

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

  Qed.

... and also lift this observation to the set of all backlogged jobs at any given time in the shared prefix.
  Lemma backlogged_jobs_prefix_invariance:
    ∀ t,
      t < h →
      jobs_backlogged_at arr_seq sched t = jobs_backlogged_at arr_seq sched' t.

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

1 subgoal (ID 698)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  ============================
  forall t : nat,
  t < h ->
  jobs_backlogged_at arr_seq sched t = jobs_backlogged_at arr_seq sched' t

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

  Proof.
    move⇒ t IN_PREFIX.

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

1 subgoal (ID 700)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : nat
  IN_PREFIX : t < h
  ============================
  jobs_backlogged_at arr_seq sched t = jobs_backlogged_at arr_seq sched' t

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

    rewrite /jobs_backlogged_at.

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

1 subgoal (ID 713)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : nat
  IN_PREFIX : t < h
  ============================
  [seq j <- arrivals_up_to arr_seq t | backlogged sched j t] =
  [seq j <- arrivals_up_to arr_seq t | backlogged sched' j t]

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

    apply eq_filter.

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

1 subgoal (ID 714)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : nat
  IN_PREFIX : t < h
  ============================
  (backlogged sched)^~ t =1 (backlogged sched')^~ t

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

    rewrite /eqfun ⇒ j.

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

1 subgoal (ID 716)
  
  Job : JobType
  H : JobCost Job
  H0 : JobArrival Job
  PState : Type
  H1 : ProcessorState Job PState
  RM : JobReady Job PState
  H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
  arr_seq : arrival_sequence Job
  sched, sched' : schedule PState
  h : instant
  H_shared_prefix : identical_prefix sched sched' h
  t : nat
  IN_PREFIX : t < h
  j : Job
  ============================
  backlogged sched j t = backlogged sched' j t

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

    now apply backlogged_prefix_invariance.

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

No more subgoals.

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

  Qed.

End NonClairvoyance.