analysis/facts/behavior/service.v

+Require Export prosa.util.all.
+Require Export prosa.behavior.all.
+Require Export prosa.analysis.definitions.schedule_prefix.
+Require Export prosa.analysis.facts.behavior.supply.
+Require Export prosa.analysis.facts.model.scheduled.
+
+
+(** * Service *)
+
+(** In this file, we establish basic facts about the service received by
+    jobs. *)
+
+(** To begin with, we provide some simple but handy rewriting rules for
+      [service] and [service_during]. *)
+Section Composition.
+
+  (** Consider any job type and any processor state. *)
+  Context {Job: JobType}.
+  Context {PState: ProcessorState Job}.
+
+  (** For any given schedule... *)
+  Variable sched: schedule PState.
+
+  (** ...and any given job... *)
+  Variable j: Job.
+
+  (** ...we establish a number of useful rewriting rules that decompose
+     the service received during an interval into smaller intervals. *)
+
+  (** As a trivial base case, no job receives any service during an empty
+     interval. *)
+  Lemma service_during_geq:
+    forall t1 t2,
+      t1 >= t2 -> service_during sched j t1 t2 = 0.
+  Proof. by move=> ? ? ?; rewrite /service_during big_geq. Qed.
+
+  (** Conversely, if a job receives some service in some interval, then the
+      interval is not empty. *)
+  Corollary service_during_ge :
+    forall t1 t2 k,
+      service_during sched j t1 t2 > k ->
+      t1 < t2.
+  Proof.
+    move=> t1 t2 k GT.
+    apply: (contraPltn _ GT) => LEQ.
+    by move: (service_during_geq _ _ LEQ) => ->.
+  Qed.
+
+  (** Equally trivially, no job has received service prior to time zero. *)
+  Corollary service0:
+    service sched j 0 = 0.
+  Proof. by rewrite /service service_during_geq. Qed.
+
+  (** Trivially, an interval consisting of one time unit is equivalent to
+     [service_at].  *)
+  Lemma service_during_instant:
+    forall t,
+      service_during sched j t t.+1 = service_at sched j t.
+  Proof. by move=> ?; rewrite /service_during big_nat_recr// big_geq. Qed.
+
+  (** Next, we observe that we can look at the service received during an
+     interval <<[t1, t3)>> as the sum of the service during [t1, t2) and [t2, t3)
+     for any t2 \in [t1, t3]. (The "_cat" suffix denotes the concatenation of
+     the two intervals.) *)
+  Lemma service_during_cat:
+    forall t1 t2 t3,
+      t1 <= t2 <= t3 ->
+      (service_during sched j t1 t2) + (service_during sched j t2 t3)
+      = service_during sched j t1 t3.
+  Proof. by move => ? ? ? /andP[? ?]; rewrite -big_cat_nat. Qed.
+
+  (** Since [service] is just a special case of [service_during], the same holds
+     for [service]. *)
+  Lemma service_cat:
+    forall t1 t2,
+      t1 <= t2 ->
+      (service sched j t1) + (service_during sched j t1 t2)
+      = service sched j t2.
+  Proof. move=> ? ? ?; exact: service_during_cat. Qed.
+
+  (** As a special case, we observe that the service during an interval can be
+     decomposed into the first instant and the rest of the interval. *)
+  Lemma service_during_first_plus_later:
+    forall t1 t2,
+      t1 < t2 ->
+      (service_at sched j t1) + (service_during sched j t1.+1 t2)
+      = service_during sched j t1 t2.
+  Proof.
+    by move=> ? ? ?; rewrite -service_during_instant service_during_cat// leqnSn.
+  Qed.
+
+  (** Symmetrically, we have the same for the end of the interval. *)
+  Lemma service_during_last_plus_before:
+    forall t1 t2,
+      t1 <= t2 ->
+      (service_during sched j t1 t2) + (service_at sched j t2)
+      = service_during sched j t1 t2.+1.
+  Proof.
+    move=> t1 t2 ?; rewrite -(service_during_cat t1 t2 t2.+1) ?leqnSn ?andbT//.
+    by rewrite service_during_instant.
+  Qed.
+
+  (** And hence also for [service]. *)
+  Corollary service_last_plus_before:
+    forall t,
+      (service sched j t) + (service_at sched j t)
+      = service sched j t.+1.
+  Proof. move=> ?; exact: service_during_last_plus_before. Qed.
+
+  (** Finally, we deconstruct the service received during an interval <<[t1, t3)>>
+     into the service at a midpoint t2 and the service in the intervals before
+     and after. *)
+  Lemma service_split_at_point:
+    forall t1 t2 t3,
+      t1 <= t2 < t3 ->
+      (service_during sched j t1 t2) + (service_at sched j t2) + (service_during sched j t2.+1 t3)
+      = service_during sched j t1 t3.
+  Proof.
+    move => t1 t2 t3 /andP[t1t2 t2t3].
+    rewrite -addnA service_during_first_plus_later// service_during_cat//.
+    by rewrite t1t2 ltnW.
+  Qed.
+
+End Composition.
+
+(** As a common special case, we establish facts about schedules in which a
+    job receives either 1 or 0 service units at all times. *)
+Section UnitService.
+
+  (** Consider any job type and any processor state. *)
+  Context {Job : JobType}.
+  Context {PState : ProcessorState Job}.
+
+  (** Let's consider a unit-service model... *)
+  Hypothesis H_unit_service: unit_service_proc_model PState.
+
+  (** ...and a given schedule. *)
+  Variable sched : schedule PState.
+
+  (** Let [j] be any job that is to be scheduled. *)
+  Variable j : Job.
+
+  (** First, we prove that the instantaneous service cannot be greater than 1, ... *)
+  Lemma service_at_most_one:
+    forall t, service_at sched j t <= 1.
+  Proof. by rewrite /service_at. Qed.
+
+  (** ... which implies that the instantaneous service always equals to 0 or 1.  *)
+  Corollary service_is_zero_or_one:
+    forall t, service_at sched j t = 0 \/ service_at sched j t = 1.
+  Proof.
+    move=> t.
+    by case: service_at (service_at_most_one t) => [|[|//]] _; [left|right].
+  Qed.
+
+  (** Next we prove that the cumulative service received by job [j] in
+      any interval of length [delta] is at most [delta]. *)
+  Lemma cumulative_service_le_delta:
+    forall t delta, service_during sched j t (t + delta) <= delta.
+  Proof.
+    move=> t delta; rewrite -[X in _ <= X](sum_of_ones t).
+    apply: leq_sum => t' _; exact: service_at_most_one.
+  Qed.
+
+  (** Conversely, we prove that if the cumulative service received by
+      job [j] in an interval of length [delta] is greater than or
+      equal to [ρ], then [ρ ≤ delta]. *)
+  Lemma cumulative_service_ge_delta :
+    forall t delta ρ,
+      ρ <= service_during sched j t (t + delta) ->
+      ρ <= delta.
+  Proof. move=> ??? /leq_trans; apply; exact: cumulative_service_le_delta. Qed.
+
+  Section ServiceIsUnitGrowthFunction.
+
+    (** We show that the service received by any job [j] during any interval is
+        a unit growth function... *)
+    Lemma service_during_is_unit_growth_function :
+      forall t0,
+        unit_growth_function (service_during sched j t0).
+    Proof.
+      move=> t0 t1.
+      have [LEQ|LT]:= leqP t0 t1; last by rewrite service_during_geq; lia.
+      rewrite addn1 -service_during_last_plus_before // leq_add2l.
+      exact: service_at_most_one.
+    Qed.
+
+    (** ... and restate the same observation in terms of [service]. *)
+    Corollary  service_is_unit_growth_function :
+      unit_growth_function (service sched j).
+    Proof. by apply: service_during_is_unit_growth_function. Qed.
+
+    (** It follows that [service_during] does not skip over any values. *)
+    Corollary exists_intermediate_service_during :
+      forall t0 t1 t2 s,
+        t0 <= t1 <= t2 ->
+        service_during sched j t0 t1 <= s < service_during sched j t0 t2 ->
+      exists t,
+        t1 <= t < t2 /\
+        service_during sched j t0 t = s.
+    Proof.
+      move=> t0 t1 t2 s /andP [t0t1 t1t2] SERV.
+      apply: exists_intermediate_point => //.
+      exact: service_during_is_unit_growth_function.
+    Qed.
+
+    (** To restate this observation in terms of [service], let [s] be any value
+       less than the service received by job [j] by time [t]. *)
+    Variable t : instant.
+    Variable s : duration.
+    Hypothesis H_less_than_s: s < service sched j t.
+
+    (** There necessarily exists an earlier time [t'] where job [j] had [s]
+       units of service. *)
+    Corollary exists_intermediate_service :
+      exists t',
+        t' < t /\
+        service sched j t' = s.
+    Proof.
+      apply: (exists_intermediate_point _ service_is_unit_growth_function 0) => //.
+      by rewrite service0.
+    Qed.
+
+  End ServiceIsUnitGrowthFunction.
+
+End UnitService.
+
+(** In this section we prove a lemma about the service received by a
+    job in a fully-consuming processor schedule. *)
+Section FullyConsumingProcessor.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobTask Job Task}.
+
+  (** Consider any kind of fully-supply-consuming processor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** We show that, given that the processor provides supply at a time
+      instant [t], the fact that a job [j] is scheduled at time [t]
+      implies that the job receives service at time [t]. Intuitively,
+      this lemma states that "inside a supply" the model is equivalent
+      to the ideal uniprocessor model. *)
+  Lemma ideal_progress_inside_supplies :
+    forall j t,
+      has_supply sched t ->
+      scheduled_at sched j t ->
+      receives_service_at sched j t.
+  Proof.
+    by move=> jo to SUP SCHED; rewrite /receives_service_at H_consumed_supply_proc_model //.
+  Qed.
+
+End FullyConsumingProcessor.
+
+(** We establish a basic fact about the monotonicity of service. *)
+Section Monotonicity.
+
+  (** Consider any job type and any processor model. *)
+  Context {Job: JobType}.
+  Context {PState: ProcessorState Job}.
+
+  (** Consider any given schedule... *)
+  Variable sched: schedule PState.
+
+  (** ...and a given job that is to be scheduled. *)
+  Variable j: Job.
+
+  (** We observe that the amount of service received is monotonic by definition. *)
+  Lemma service_monotonic:
+    forall t1 t2,
+      t1 <= t2 ->
+      service sched j t1 <= service sched j t2.
+  Proof. by move=> t1 t2 ?; rewrite -(service_cat _ _ t1 t2)// leq_addr. Qed.
+
+End Monotonicity.
+
+(** In the following, we establish a collection of facts relating
+    service with predicates [scheduled_in] and [scheduled_at]. *)
+Section RelationToScheduled.
+
+  (** Consider any job type and any processor model. *)
+  Context {Job: JobType}.
+  Context {PState: ProcessorState Job}.
+
+  (** Consider any given schedule... *)
+  Variable sched: schedule PState.
+
+  (** ...and a given job that is to be scheduled. *)
+  Variable j: Job.
+
+  (** We observe that a job that isn't scheduled in a given processor
+      state cannot possibly receive service in that state. *)
+  Lemma service_in_implies_scheduled_in :
+    forall s,
+      ~~ scheduled_in j s -> service_in j s = 0.
+  Proof.
+    move=> s.
+    move=> /existsP Hsched; apply/eqP; rewrite sum_nat_eq0; apply/forallP => c.
+    rewrite service_on_implies_scheduled_on//.
+    by apply/negP => ?; apply: Hsched; exists c.
+  Qed.
+
+  (** In particular, it cannot receive service at any given time. *)
+  Corollary not_scheduled_implies_no_service:
+    forall t,
+      ~~ scheduled_at sched j t -> service_at sched j t = 0.
+  Proof. move=> ?; exact: service_in_implies_scheduled_in. Qed.
+
+  (** Similarly, if a job is not scheduled during an interval, then it
+      does not receive any service in that interval. *)
+  Lemma not_scheduled_during_implies_zero_service:
+    forall t1 t2,
+      (forall t, t1 <= t < t2 -> ~~ scheduled_at sched j t) ->
+      service_during sched j t1 t2 = 0.
+  Proof.
+    move=> t1 t2; rewrite big_nat_eq0 => + t titv => /(_ t titv).
+    by apply not_scheduled_implies_no_service.
+  Qed.
+
+  (** Conversely, if the job's instantaneous received service is
+      positive, then it must be scheduled. *)
+  Lemma service_at_implies_scheduled_at :
+    forall t,
+      service_at sched j t > 0 -> scheduled_at sched j t.
+  Proof.
+    move=> t; case SCHEDULED: scheduled_at => //.
+    by rewrite not_scheduled_implies_no_service// negbT.
+  Qed.
+
+  (** Thus, if the cumulative amount of service changes, then it must
+      be scheduled, too. *)
+  Lemma service_delta_implies_scheduled :
+    forall t,
+      service sched j t < service sched j t.+1 -> scheduled_at sched j t.
+  Proof.
+    move=> t; rewrite -service_last_plus_before -ltn_subLR// subnn.
+    exact: service_at_implies_scheduled_at.
+  Qed.
+
+  (** We observe that a job receives cumulative service during some interval iff
+     it receives services at some specific time in the interval. *)
+  Lemma service_during_service_at :
+    forall t1 t2,
+      service_during sched j t1 t2 > 0
+      <->
+      exists t,
+        t1 <= t < t2 /\
+        service_at sched j t > 0.
+  Proof.
+    move=> t1 t2.
+    split=> [|[t [titv nz_serv]]].
+    - rewrite sum_nat_gt0 filter_predT => /hasP [t IN GT0].
+      by exists t; split; [rewrite -mem_index_iota|].
+    - rewrite sum_nat_gt0; apply/hasP.
+      by exists t; [rewrite filter_predT mem_index_iota|].
+  Qed.
+
+  (** Thus, any job that receives some service during an interval must be
+      scheduled at some point during the interval... *)
+  Corollary cumulative_service_implies_scheduled :
+    forall t1 t2,
+      service_during sched j t1 t2 > 0 ->
+      exists t,
+        t1 <= t < t2 /\
+        scheduled_at sched j t.
+  Proof.
+    move=> t1 t2; rewrite service_during_service_at => -[t' [TIMES SERVICED]].
+    exists t'; split=> //; exact: service_at_implies_scheduled_at.
+  Qed.
+
+  (** ...which implies that any job with positive cumulative service must have
+     been scheduled at some point. *)
+  Corollary positive_service_implies_scheduled_before:
+    forall t,
+      service sched j t > 0 -> exists t', (t' < t /\ scheduled_at sched j t').
+  Proof.
+    by move=> t /cumulative_service_implies_scheduled[t' ?]; exists t'.
+  Qed.
+
+  (** We can further strengthen [service_during_service_at] to yield the
+      earliest point in time at which a job receives service in an interval... *)
+  Corollary service_during_service_at_earliest :
+    forall t1 t2,
+      service_during sched j t1 t2 > 0 ->
+      exists t,
+        t1 <= t < t2
+        /\ service_at sched j t > 0
+        /\ service_during sched j t1 t = 0.
+  Proof.
+    move=> t1 t2.
+    rewrite service_during_service_at => [[t [IN SAT]]].
+    set P := fun t' => (service_at sched j t' > 0) && (t1 <= t' < t2).
+    have WITNESS: exists t', P t' by exists t; apply/andP.
+    have [t' /andP [SCHED' IN'] LEAST] := ex_minnP WITNESS.
+    exists t'; repeat (split => //).
+    apply/eqP/contraT.
+    rewrite -lt0n service_during_service_at => [[t'' [IN'' SAT'']]].
+    have: t' <= t''; last by lia.
+    apply/LEAST/andP; split => //.
+    by lia.
+  Qed.
+
+  (** ... and make a similar observation about the same point in time
+      w.r.t. [scheduled_at]. *)
+  Corollary service_during_scheduled_at_earliest :
+    forall t1 t2,
+      service_during sched j t1 t2 > 0 ->
+      exists t,
+        t1 <= t < t2
+        /\ scheduled_at sched j t
+        /\ service_during sched j t1 t = 0.
+  Proof.
+    move=> t1 t2 SERVICED.
+    have [t [IN [SAT NONE]]] := service_during_service_at_earliest t1 t2 SERVICED.
+    exists t; repeat (split => //).
+    exact: service_at_implies_scheduled_at.
+  Qed.
+
+  (** If we can assume that a scheduled job always receives service, then we can
+      further relate above observations to [scheduled_at]. *)
+  Section GuaranteedService.
+
+    (** Assume [j] always receives some positive service. *)
+    Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
+
+    (** In other words, not being scheduled is equivalent to receiving zero
+       service. *)
+    Lemma no_service_not_scheduled:
+      forall t,
+        ~~ scheduled_at sched j t <-> service_at sched j t = 0.
+    Proof.
+      move=> t.
+      split => [|NO_SERVICE]; first exact: service_in_implies_scheduled_in.
+      apply: (contra (H_scheduled_implies_serviced j (sched t))).
+      by rewrite -eqn0Ngt -NO_SERVICE.
+    Qed.
+
+    (** Then, if a job does not receive any service during an interval, it
+       is not scheduled. *)
+    Lemma no_service_during_implies_not_scheduled:
+      forall t1 t2,
+        service_during sched j t1 t2 = 0 ->
+        forall t,
+          t1 <= t < t2 -> ~~ scheduled_at sched j t.
+    Proof.
+      move=> t1 t2.
+      by move=> + t titv; rewrite no_service_not_scheduled big_nat_eq0; apply.
+    Qed.
+
+    (** If a job is scheduled at some point in an interval, it receives
+       positive cumulative service during the interval... *)
+    Lemma scheduled_implies_cumulative_service:
+      forall t1 t2,
+        (exists t,
+            t1 <= t < t2 /\
+            scheduled_at sched j t) ->
+        service_during sched j t1 t2 > 0.
+    Proof.
+      move=> t1 t2 [t [titv sch]]; rewrite service_during_service_at.
+      exists t; split=> //; exact: H_scheduled_implies_serviced.
+    Qed.
+
+    (** ...which again applies to total service, too. *)
+    Corollary scheduled_implies_nonzero_service:
+      forall t,
+        (exists t',
+            t' < t /\
+            scheduled_at sched j t') ->
+        service sched j t > 0.
+    Proof.
+      move=> t.
+      by move=> [t' ?]; apply: scheduled_implies_cumulative_service; exists t'.
+    Qed.
+
+  End GuaranteedService.
+
+  (** Furthermore, if we know that jobs are not released early, then we can
+      narrow the interval during which they must have been scheduled. *)
+  Section AfterArrival.
+
+    Context `{JobArrival Job}.
+
+    (** Assume that jobs must arrive to execute. *)
+    Hypothesis H_jobs_must_arrive:
+      jobs_must_arrive_to_execute sched.
+
+    (** We prove that any job with positive cumulative service at time [t] must
+       have been scheduled some time since its arrival and before time [t]. *)
+    Lemma positive_service_implies_scheduled_since_arrival:
+      forall t,
+        service sched j t > 0 ->
+        exists t', (job_arrival j <= t' < t /\ scheduled_at sched j t').
+    Proof.
+      move=> t /positive_service_implies_scheduled_before[t' [t't sch]].
+      exists t'; split=> //; rewrite t't andbT; exact: H_jobs_must_arrive.
+    Qed.
+
+    Lemma not_scheduled_before_arrival:
+      forall t, t < job_arrival j -> ~~ scheduled_at sched j t.
+    Proof.
+      by move=> t ?; apply: (contra (H_jobs_must_arrive j t)); rewrite -ltnNge.
+    Qed.
+
+    (** We show that job [j] does not receive service at any time [t] prior to its
+        arrival. *)
+    Lemma service_before_job_arrival_zero:
+      forall t,
+        t < job_arrival j ->
+        service_at sched j t = 0.
+    Proof.
+      move=> t NOT_ARR; rewrite not_scheduled_implies_no_service//.
+      exact: not_scheduled_before_arrival.
+    Qed.
+
+    (** Note that the same property applies to the cumulative service. *)
+    Lemma cumulative_service_before_job_arrival_zero :
+      forall t1 t2 : instant,
+        t2 <= job_arrival j ->
+        service_during sched j t1 t2 = 0.
+    Proof.
+      move=> t1 t2 early; rewrite big_nat_eq0 => t /andP[_ t_lt_t2].
+      apply: service_before_job_arrival_zero; exact: leq_trans early.
+    Qed.
+
+    (** Hence, one can ignore the service received by a job before its arrival
+       time... *)
+    Lemma ignore_service_before_arrival:
+      forall t1 t2,
+        t1 <= job_arrival j ->
+        t2 >= job_arrival j ->
+        service_during sched j t1 t2 = service_during sched j (job_arrival j) t2.
+    Proof.
+      move=> t1 t2 t1_le t2_ge.
+      rewrite -(service_during_cat sched _ _ (job_arrival j)); last exact/andP.
+      by rewrite cumulative_service_before_job_arrival_zero.
+    Qed.
+
+    (** ... which we can also state in terms of cumulative service. *)
+    Corollary no_service_before_arrival:
+      forall t,
+        t <= job_arrival j -> service sched j t = 0.
+    Proof. exact: cumulative_service_before_job_arrival_zero. Qed.
+
+  End AfterArrival.
+
+  (** In this section, we prove some lemmas about time instants with same
+      service. *)
+  Section TimesWithSameService.
+
+    (** Consider any time instants [t1] and [t2]... *)
+    Variable t1 t2: instant.
+
+    (** ...where [t1] is no later than [t2]... *)
+    Hypothesis H_t1_le_t2: t1 <= t2.
+
+    (** ...and where job [j] has received the same amount of service. *)
+    Hypothesis H_same_service: service sched j t1 = service sched j t2.
+
+    (** First, we observe that this means that the job receives no service
+       during <<[t1, t2)>>... *)
+    Lemma constant_service_implies_no_service_during:
+      service_during sched j t1 t2 = 0.
+    Proof.
+      move: H_same_service; rewrite -(service_cat _ _ t1 t2)// => /eqP.
+      by rewrite -[X in X == _]addn0 eqn_add2l => /eqP.
+    Qed.
+
+    (** ...which of course implies that it does not receive service at any
+       point, either. *)
+    Lemma constant_service_implies_not_scheduled:
+      forall t,
+        t1 <= t < t2 -> service_at sched j t = 0.
+    Proof.
+      move=> t titv.
+      have := constant_service_implies_no_service_during.
+      rewrite big_nat_eq0; exact.
+    Qed.
+
+    (** We show that job [j] receives service at some point [t < t1]
+       iff [j] receives service at some point [t' < t2]. *)
+    Lemma same_service_implies_serviced_at_earlier_times:
+      [exists t: 'I_t1, service_at sched j t > 0] =
+      [exists t': 'I_t2, service_at sched j t' > 0].
+    Proof.
+      apply/idP/idP => /existsP[t serv].
+      { by apply/existsP; exists (widen_ord H_t1_le_t2 t). }
+      have [t_lt_t1|t1_le_t] := ltnP t t1.
+      { by apply/existsP; exists (Ordinal t_lt_t1). }
+      exfalso; move: serv; apply/negP; rewrite -eqn0Ngt.
+      by apply/eqP/constant_service_implies_not_scheduled; rewrite t1_le_t /=.
+    Qed.
+
+    (** Then, under the assumption that scheduled jobs receives service,
+        we can translate this into a claim about scheduled_at. *)
+
+    (** Assume [j] always receives some positive service. *)
+    Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
+
+    (** We show that job [j] is scheduled at some point [t < t1] iff [j] is scheduled
+       at some point [t' < t2].  *)
+    Lemma same_service_implies_scheduled_at_earlier_times:
+      [exists t: 'I_t1, scheduled_at sched j t] =
+      [exists t': 'I_t2, scheduled_at sched j t'].
+    Proof.
+      have CONV B : [exists b: 'I_B, scheduled_at sched j b]
+                    = [exists b: 'I_B, service_at sched j b > 0].
+      { apply/idP/idP => /existsP[b P]; apply/existsP; exists b.
+        - exact: H_scheduled_implies_serviced.
+        - exact: service_at_implies_scheduled_at. }
+      by rewrite !CONV same_service_implies_serviced_at_earlier_times.
+    Qed.
+
+  End TimesWithSameService.
+
+End RelationToScheduled.
+
+(** In this section we prove a few auxiliary lemmas about the service
+    received by a job. *)
+Section GenericProcessor.
+
+  (** Consider any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of processor state model. *)
+  Context `{PState : ProcessorState Job}.
+
+  (** Consider any valid arrival sequence with consistent arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any schedule of this arrival sequence ... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence :
+    jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival or after
+      completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** If a job [j] receives service at time [t], then [j] is in the
+      set of served jobs at time [t] ... *)
+  Lemma receives_service_and_served_at_consistent :
+    forall j t,
+      receives_service_at sched j t ->
+      j \in served_jobs_at arr_seq sched t.
+  Proof.
+    move=> jo t RSERV; rewrite mem_filter; apply/andP; split => //.
+    apply service_at_implies_scheduled_at in RSERV.
+    by apply: arrivals_before_scheduled_at.
+  Qed.
+
+  (** ... and vice versa, if [j] is in the set of jobs receiving
+      service at time [t], then [j] receives service at time [t]. *)
+  Lemma served_at_and_receives_service_consistent :
+    forall j t,
+      j \in served_jobs_at arr_seq sched t ->
+      receives_service_at sched j t.
+  Proof.
+    by move=> jo t; rewrite mem_filter => /andP [RSERV _].
+  Qed.
+
+  (** If the processor is idle at time [t], then no job receives
+      service at time [t]. *)
+  Lemma no_service_received_when_idle :
+    forall j t,
+      is_idle arr_seq sched t ->
+      ~~ receives_service_at sched j t.
+  Proof.
+    move=> j t IDLE; apply/negP => SERV.
+    eapply not_scheduled_when_idle with (j := j) in IDLE => //.
+    apply service_at_implies_scheduled_at in SERV.
+    by rewrite SERV in IDLE.
+  Qed.
+
+  (** Next, if a job [j] receives service at time [t],
+      then the processor has supply at time [t]. *)
+  Lemma receives_service_implies_has_supply :
+    forall j t,
+      receives_service_at sched j t ->
+      has_supply sched t.
+  Proof.
+    by move=> j SERV; apply: pos_service_impl_pos_supply.
+  Qed.
+
+  (** Similarly, if a job [j] receives service at time [t], then time
+      [t] is not a blackout time. *)
+  Lemma no_blackout_when_service_received :
+    forall j t,
+      receives_service_at sched j t ->
+      ~~ is_blackout sched t.
+  Proof.
+    by move=> j t RSERV; apply pos_service_impl_pos_supply in RSERV; rewrite negbK.
+  Qed.
+
+  (** Finally, if time [t] is a blackout time, then no job receives
+      service at time [t]. *)
+  Lemma no_service_during_blackout :
+    forall j t,
+      is_blackout sched t ->
+      service_at sched j t = 0.
+  Proof.
+    move=> j t BL; apply/eqP; rewrite -leqn0; move_neq_up GE.
+    apply pos_service_impl_pos_supply in GE.
+    by rewrite /is_blackout /has_supply GE in BL.
+  Qed.
+
+End GenericProcessor.
+
+(** In this section we prove a lemma about the service received by a
+    job in a uniprocessor schedule. *)
+Section UniProcessor.
+
+  (** Consider any type of jobs. *)
+  Context {Job : JobType}.
+
+  (** Consider any kind of uniprocessor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+
+  (** Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  (** If two jobs [j1] and [j2] receive service at the same instant
+      then [j1] is equal to [j2]. *)
+  Lemma only_one_job_receives_service_at_uni :
+    forall j1 j2 t,
+      receives_service_at sched j1 t ->
+      receives_service_at sched j2 t ->
+      j1 = j2.
+  Proof.
+    move => j1 j2 t SERV1 SERV2.
+    apply service_at_implies_scheduled_at in SERV1.
+    apply service_at_implies_scheduled_at in SERV2.
+    by apply (H_uniprocessor_proc_model j1 j2 sched t).
+  Qed.
+
+End UniProcessor.
+
+(** * Incremental Service in Unit-Service Schedules  *)
+(** In unit-service schedules, any job gains at most one unit of service at any
+    time. Hence, no job "skips" an service values, which we note with the lemma
+    [incremental_service_during] below. *)
+Section IncrementalService.
+
+  (** Consider any job type, ... *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any unit-service schedule of this arrival sequence. *)
+  Context {PState : ProcessorState Job}.
+  Variable sched : schedule PState.
+  Hypothesis H_unit_service: unit_service_proc_model PState.
+
+  (** We prove that if in some time interval <<[t1,t2)>> a job [j] receives [k]
+      units of service, then there exists a time instant <<t ∈ [t1,t2)>> such
+      that [j] is scheduled at time [t] and service of job [j] within interval
+      <<[t1,t)>> is equal to [k]. *)
+  Lemma incremental_service_during :
+    forall j t1 t2 k,
+      service_during sched j t1 t2 > k ->
+      exists t, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.
+  Proof.
+    move=> j t1 t2 k SERV.
+    have LE: t1 < t2 by move: (service_during_ge _ _ _ _ _ SERV).
+    case: k SERV => [|k] SERV; first by apply service_during_scheduled_at_earliest in SERV.
+    set P := fun t' => service_during sched j t1 t' >= k.+1.
+    have: exists t' : nat, t1 < t' <= t2 /\ (forall x : nat, t1 <= x < t' -> ~~ P x) /\ P t'.
+    { apply: (exists_first_intermediate_point P t1 t2); first by lia.
+      - by rewrite /P service_during_geq //.
+      - by rewrite /P;  lia. }
+    rewrite /P; move=> [t' [IN' [LIMIT Pt']]]; clear P.
+    set P'' := fun t'' => (t' <= t'' < t2) && (service_at sched j t'' > 0).
+    have WITNESS: exists t'', P'' t''.
+    { have: 0 < service_during sched j t' t2;
+        last by rewrite service_during_service_at => [[t'' [IN'' SERVICED]]]
+                ; exists t''; apply/andP; split.
+      move: SERV; rewrite -(service_during_cat _ _ t1 t'.-1 t2); last by lia. move=> SERV.
+      have SERV2: service_during sched j t1 t'.-1 <= k
+        by rewrite leqNgt; apply (LIMIT t'.-1); lia.
+      have: service_during sched j t'.-1 t2 >= 2 by lia.
+      rewrite -service_during_first_plus_later; last by lia.
+      move: (IN') => /andP [LE' _]; rewrite (ltn_predK LE').
+      by case: (service_is_zero_or_one _ sched j t'.-1) =>  [//|->|->]; try lia. }
+    have [t''' /andP [IN''' SCHED'''] MIN] := ex_minnP WITNESS.
+    exists t'''; repeat split; [by lia|by apply: service_at_implies_scheduled_at|].
+    have ->:  service_during sched j t1 t''' = service_during sched j t1 t'.
+    { rewrite -(service_during_cat _ _ t1 t' t'''); last by lia.
+      have [Z|POS] := leqP (service_during sched j t' t''') 0; first by lia.
+      exfalso.
+      move: POS; rewrite service_during_service_at => [[x [xIN xSERV]]].
+      have xP'': P'' x by apply/andP;split; [by lia| by[]].
+      by move: (MIN x xP''); lia. }
+    move: Pt'; rewrite leq_eqVlt => /orP [/eqP -> //|XL].
+    exfalso. move: XL.
+    have ->: service_during sched j t1 t' = service_during sched j t1 t'.-1.+1
+      by move: (IN') => /andP [LE' _]; rewrite (ltn_predK LE').
+    rewrite -service_during_last_plus_before; last by lia. move=> ABOVE.
+    have BELOW: service_during sched j t1 t'.-1 <= k
+      by rewrite leqNgt; apply (LIMIT t'.-1); lia.
+    have: service_at sched j t'.-1 > 1 by lia.
+    have: service_at sched j t'.-1 <= 1 by apply/service_at_most_one.
+    by lia.
+  Qed.
+
+  (** An implication of the above lemma is that for any job [j] that
+      has [k] units of service at time [t] and more than [k] units of
+      service at time [t'], there exists a time instant [st] such that
+      [t <= st < t'] and the job is scheduled but still has [k] units
+      of service. *)
+  Lemma kth_scheduling_time :
+    forall j t t' k,
+      service sched j t = k ->
+      k < service sched j t' ->
+      exists st,
+        t <= st < t'
+        /\ service sched j st = k
+        /\ scheduled_at sched j st.
+  Proof.
+    move=> j t t' σ SERVEQ GT.
+    have LT : t <= t'.
+    { move_neq_up LT.
+      rewrite -(service_cat _ _ t') in SERVEQ; last by lia.
+      move_neq_down GT.
+      by rewrite -SERVEQ leq_addr. }
+    have POS : service_during sched j t t' > 0.
+    { rewrite -(service_cat _ _ t) in GT; last by done.
+      by rewrite SERVEQ -addn1 leq_add2l in GT. }
+    apply service_during_service_at_earliest in POS.
+    move: POS => [st [/andP [NEQ1 NEQ2 ] [SERV SDZ]]].
+    exists st; split; [by lia | split].
+    { erewrite <-service_cat; last by apply: NEQ1.
+      by rewrite SERVEQ SDZ addn0. }
+    { by apply service_at_implies_scheduled_at. }
+  Qed.
+
+End IncrementalService.
+
+
+Section ServiceInTwoSchedules.
+
+  (** Consider any job type and any processor model. *)
+  Context {Job: JobType}.
+  Context {PState: ProcessorState Job}.
+
+  (** Consider any two given schedules... *)
+  Variable sched1 sched2: schedule PState.
+
+  (** Given an interval in which the schedules provide the same service
+      to a job at each instant, we can prove that the cumulative service
+      received during the interval has to be the same. *)
+  Section ServiceDuringEquivalentInterval.
+
+    (** Consider two time instants...  *)
+    Variable t1 t2 : instant.
+
+    (** ...and a given job that is to be scheduled. *)
+    Variable j: Job.
+
+    (** Assume that, in any instant between [t1] and [t2] the service
+        provided to [j] from the two schedules is the same. *)
+    Hypothesis H_sched1_sched2_same_service_at:
+      forall t, t1 <= t < t2 ->
+           service_at sched1 j t = service_at sched2 j t.
+
+    (** It follows that the service provided during [t1] and [t2]
+        is also the same. *)
+    Lemma same_service_during:
+      service_during sched1 j t1 t2 = service_during sched2 j t1 t2.
+    Proof. exact/eq_big_nat/H_sched1_sched2_same_service_at. Qed.
+
+  End ServiceDuringEquivalentInterval.
+
+  (** We can leverage the previous lemma to conclude that two schedules
+      that match in a given interval will also have the same cumulative
+      service across the interval. *)
+  Corollary equal_prefix_implies_same_service_during:
+    forall t1 t2,
+      (forall t, t1 <= t < t2 -> sched1 t = sched2 t) ->
+      forall j, service_during sched1 j t1 t2 = service_during sched2 j t1 t2.
+  Proof.
+    move=> t1 t2 sch j; apply: same_service_during => t' t'itv.
+    by rewrite /service_at sch.
+  Qed.
+
+  (** For convenience, we restate the corollary also at the level of
+      [service] for identical prefixes. *)
+  Corollary identical_prefix_service:
+    forall h,
+      identical_prefix sched1 sched2 h ->
+      forall j, service sched1 j h = service sched2 j h.
+  Proof. move=> ? ? ?; exact: equal_prefix_implies_same_service_during. Qed.
+
+End ServiceInTwoSchedules.
+
+  (** We add some facts into the "Hint Database" basic_rt_facts, so
+      Coq will be able to apply them automatically where needed. *)
+Global Hint Resolve
+       served_at_and_receives_service_consistent
+  : basic_rt_facts.

analysis/facts/behavior/supply.v

+Require Export prosa.util.all.
+Require Export prosa.model.processor.platform_properties.
+
+(** * Supply *)
+(** In this file, we establish properties of the notion of supply. *)
+
+(** We start with a few basic facts about supply. *)
+Section BasicFacts.
+
+  (** Consider any type of jobs, ... *)
+  Context {Job : JobType}.
+
+  (** ... any kind of processor state model, ... *)
+  Context `{PState : ProcessorState Job}.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** First, we leverage the property [service_on_le_supply_on] to
+      show that [service_at j t] is always bounded by [supply_at
+      t]. *)
+  Lemma service_at_le_supply_at :
+    forall j t,
+      service_at sched j t <= supply_at sched t.
+  Proof.
+    by move=> j t; apply: leq_sum => c _; apply service_on_le_supply_on.
+  Qed.
+
+  (** As a corollary, it is easy to show that if a job receives
+      service at a time instant [t], then the supply at this time
+      instant is positive. *)
+  Corollary pos_service_impl_pos_supply :
+    forall j t,
+      0 < service_at sched j t ->
+      0 < supply_at sched t.
+  Proof.
+    by move=> j t; rewrite (leqRW (service_at_le_supply_at _ _)).
+  Qed.
+
+  (** Next, we show that, at any time instant [t], either there is
+      some supply available or it is a blackout time. *)
+  Lemma blackout_or_supply :
+    forall t,
+      is_blackout sched t \/ has_supply sched t.
+  Proof.
+    by rewrite /is_blackout; move=> t; case: (has_supply).
+  Qed.
+
+End BasicFacts.
+
+(** As a common special case, we establish facts about schedules in
+    which supply is either 0 or 1 at all times. *)
+Section UnitService.
+
+  (** Consider any type of jobs, ... *)
+  Context {Job : JobType}.
+
+  (** ... any kind of unit-supply processor state model, ... *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** We show that, under the unit-supply assumption, [supply_at t] is
+      equal to [1 - is_blackout t] for any time instant [t]. *)
+  Lemma supply_at_complement :
+    forall t,
+      supply_at sched t = 1 - is_blackout sched t.
+  Proof.
+    move=> t; have := H_unit_supply_proc_model (sched t).
+    by rewrite /is_blackout /has_supply /supply_at; case: supply_in => [|[]].
+  Qed.
+
+  (** We note that supply is bounded at all times by [1] ... *)
+  Remark supply_at_le_1 :
+    forall t,
+      supply_at sched t <= 1.
+  Proof. by move=> t; apply H_unit_supply_proc_model. Qed.
+
+  (** ... and as a trivial consequence, we show that the service of
+      any job is either [0] or [1]. *)
+  Corollary unit_supply_proc_service_case :
+    forall j t,
+      service_at sched j t = 0 \/ service_at sched j t = 1.
+  Proof.
+    move=> j t.
+    have SER := service_at_le_supply_at sched j t.
+    have SUP := supply_at_le_1 t.
+    by lia.
+  Qed.
+
+  (** We show that supply during an interval <<[t, t + δ)>> is bounded by [δ]. *)
+  Lemma supply_during_bound :
+    forall t δ,
+      supply_during sched t (t + δ) <= δ.
+  Proof.
+    move=> t d; rewrite -[leqRHS](addKn t) -[leqRHS]muln1 -sum_nat_const_nat.
+    by apply: leq_sum => t0 _;  apply supply_at_le_1.
+  Qed.
+
+  (** We observe that the supply during an interval can be decomposed
+      into the last instant and the rest of the interval. *)
+  Lemma supply_during_last_plus_before :
+    forall t1 t2,
+      t1 <= t2 ->
+      supply_during sched t1 t2.+1 = supply_during sched t1 t2 + supply_at sched t2.
+  Proof. by move => t1 t2 LEQ; rewrite /supply_during big_nat_recr //=. Qed.
+
+  (** Finally, we show that the blackout during a time interval <<[t,
+      t + δ)>> is equal to the difference between [δ] and the supply
+      during <<[t, t + δ)>>. *)
+  Lemma blackout_during_complement :
+    forall t δ,
+      blackout_during sched t (t + δ) = δ - supply_during sched t (t + δ).
+  Proof.
+    move=> t; elim=> [|δ IHδ]; first by rewrite addn0 [LHS]big_geq.
+    rewrite addnS [LHS]big_nat_recr ?leq_addr//= [X in X + _]IHδ.
+    rewrite supply_during_last_plus_before ?leq_addr// supply_at_complement.
+    by rewrite -addn1 subnACA ?supply_during_bound; lia.
+  Qed.
+
+End UnitService.
+
+(** Lastly, we prove one lemma about supply in the case of the fully
+    supply-consuming processor model. *)
+Section ConsumedSupply.
+
+  (** Consider any type of jobs, ... *)
+  Context {Job : JobType}.
+
+  (** ... any kind of fully supply-consuming processor state model, ... *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_supply_is_fully_consumed : fully_consuming_proc_model PState.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** The fact that a job [j] is scheduled at a time instant [t] and
+      there is a supply at [t] implies that the job receives service
+      at time [t]. *)
+  Lemma progress_inside_supplies :
+    forall (j : Job) (t : instant),
+      has_supply sched t ->
+      scheduled_at sched j t ->
+      0 < service_at sched j t.
+  Proof.
+    by move => j t SUP SCHED; rewrite H_supply_is_fully_consumed.
+  Qed.
+
+End ConsumedSupply.
+
+(** We add some of the above lemmas to the "Hint Database"
+    [basic_rt_facts], so the [auto] tactic will be able to use
+    them. *)
+Global Hint Resolve
+       supply_at_le_1
+  : basic_rt_facts.

analysis/facts/blocking_bound/edf.v

+Require Export prosa.analysis.definitions.blocking_bound.edf.
+Require Export prosa.analysis.facts.busy_interval.pi.
+Require Export prosa.model.priority.edf.
+Require Export prosa.model.task.absolute_deadline.
+Require Export prosa.analysis.facts.model.arrival_curves.
+
+(** * Lower-Priority Non-Preemptive Segment is Bounded *)
+(** In this file, we prove that, under the EDF scheduling policy, the
+    length of the maximum non-preemptive segment of a lower-priority
+    job (w.r.t. a job of a task [tsk]) is bounded by
+    [blocking_bound]. *)
+Section  MaxNPSegmentIsBounded.
+
+  (** Consider any type of tasks, each characterized by a WCET
+      [task_cost], an arrival curve [max_arrivals], a relative
+      deadline [task_deadline], and a bound on the the task's longest
+      non-preemptive segment [task_max_nonpreemptive_segment] ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{MaxArrivals Task}.
+  Context `{TaskDeadline Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (** ... and any type of jobs associated with these tasks, where each
+      job has a task [job_task], a cost [job_cost], and an arrival
+      time [job_arrival]. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+
+  (** Consider any kind of processor state model. *)
+  Context `{PState : ProcessorState Job}.
+
+  (** Consider the EDF policy. *)
+  Let EDF := EDF Job.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** We further require that a job's cost cannot exceed its task's stated WCET ... *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** ... and assume that jobs have bounded non-preemptive segments. *)
+  Context `{JobPreemptable Job}.
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Consider an arbitrary task set [ts], ... *)
+  Variable ts : seq Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** ... and let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Let [max_arrivals] be a family of arrival curves. *)
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Consider any job [j] of [tsk]. *)
+  Variable j : Job.
+  Hypothesis H_job_of_tsk : job_of_task tsk j.
+
+  (** Then, the maximum length of a nonpreemptive segment among all
+      lower-priority jobs (w.r.t. the given job [j]) arrived so far is
+      bounded by [blocking_bound]. *)
+  Lemma nonpreemptive_segments_bounded_by_blocking :
+    forall t1 t2,
+      busy_interval_prefix arr_seq sched j t1 t2 ->
+      max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound ts tsk (job_arrival j - t1).
+  Proof.
+    move=> t1 t2 BUSY; rewrite /max_lp_nonpreemptive_segment /blocking_bound.
+    apply: leq_trans;first by exact: max_np_job_segment_bounded_by_max_np_task_segment.
+    apply /bigmax_leq_seqP => j' JINB NOTHEP.
+    have ARR': arrives_in arr_seq j'
+      by apply: in_arrivals_implies_arrived; exact: JINB.
+    apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1);
+      first by apply H_all_jobs_from_taskset.
+    apply in_arrivals_implies_arrived_between in JINB => [|//].
+    move: JINB; move => /andP [_ TJ'].
+    repeat (apply/andP; split); last first.
+    { rewrite /hep_job -ltnNge in NOTHEP.
+      move: H_job_of_tsk => /eqP <-.
+      have ARRLE: job_arrival j' < job_arrival j.
+      { by apply: (@leq_trans t1) => //; move: BUSY => [ _  [ _ [ _ /andP [F G]]] ]. } 
+      move: NOTHEP; rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline.
+      by lia. }
+    { move: NOTHEP => /andP [_ NZ].
+      move: (H_valid_job_cost j' ARR'); rewrite /valid_job_cost.
+      by lia. }
+    { apply: non_pathological_max_arrivals; last first.
+      - exact: ARR'.
+      - by rewrite /job_of_task.
+      - by apply H_is_arrival_curve, H_all_jobs_from_taskset, ARR'. }
+  Qed.
+
+End MaxNPSegmentIsBounded.

analysis/facts/blocking_bound/elf.v

+Require Export prosa.analysis.definitions.blocking_bound.elf.
+Require Export prosa.analysis.facts.busy_interval.pi.
+Require Export prosa.model.task.absolute_deadline.
+Require Export prosa.analysis.facts.model.arrival_curves.
+Require Import prosa.analysis.facts.priority.classes.
+Require Export prosa.analysis.facts.priority.elf.
+
+(** * Lower-Priority Non-Preemptive Segment is Bounded *)
+(** In this file, we prove that, under the ELF scheduling policy, the
+    length of the maximum non-preemptive segment of a lower-priority
+    job (w.r.t. a job of a task [tsk]) is bounded by
+    [blocking_bound]. *)
+Section MaxNPSegmentIsBounded.
+
+  (** Consider any type of tasks, each characterized by a WCET
+      [task_cost], an arrival curve [max_arrivals], a relative
+      deadline [task_deadline], a bound on the the task's longest
+      non-preemptive segment [task_max_nonpreemptive_segment] and
+      relative priority points, ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{MaxArrivals Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+  Context `{PriorityPoint Task}.
+
+  (** ... and any type of jobs associated with these tasks, where each
+      job has a task [job_task], a cost [job_cost], and an arrival
+      time [job_arrival]. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+
+  (** Consider any kind of processor state model. *)
+  Context `{PState : ProcessorState Job}.
+
+  (** Consider any valid arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** We further require that a job's cost cannot exceed its task's stated WCET ... *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** ... and assume that jobs have bounded non-preemptive segments. *)
+  Context `{JobPreemptable Job}.
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Consider an arbitrary task set [ts], ... *)
+  Variable ts : seq Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** ... and let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Let [max_arrivals] be a family of arrival curves. *)
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Consider any job [j] of [tsk]. *)
+  Variable j : Job.
+  Hypothesis H_job_of_tsk : job_of_task tsk j.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority
+      relation, and assume that the relation is reflexive, transitive
+      and total. *)
+  Context (FP : FP_policy Task).
+  Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.
+  Hypothesis H_transitive_priorities : transitive_task_priorities FP.
+  Hypothesis H_total_priorities : total_task_priorities FP.
+
+  (** Then, the maximum length of a nonpreemptive segment among all
+      lower-priority jobs (w.r.t. the given job [j]) arrived so far is
+      bounded by [blocking_bound]. *)
+  Lemma nonpreemptive_segments_bounded_by_blocking :
+    forall t1 t2,
+      busy_interval_prefix arr_seq sched j t1 t2 ->
+      max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound ts tsk (job_arrival j - t1).
+  Proof.
+    move=> t1 t2 BUSY; rewrite /max_lp_nonpreemptive_segment /blocking_bound //.
+    apply: leq_trans; first by apply: max_np_job_segment_bounded_by_max_np_task_segment.
+    apply /bigmax_leq_seqP => j' JINB NOTHEP.
+    have ARR': arrives_in arr_seq j'
+      by apply: in_arrivals_implies_arrived; exact: JINB.
+    apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1);
+      first by apply H_all_jobs_from_taskset.
+    apply in_arrivals_implies_arrived_between in JINB => //.
+    move: JINB; move => /andP [_ TJ'].
+    have ->: (max_arrivals (job_task j') ε > 0) && (task_cost (job_task j') > 0) = true.
+    { apply /andP; split.
+      { apply: non_pathological_max_arrivals; last first.
+        - exact: ARR'.
+        - by rewrite /job_of_task.
+        - by apply H_is_arrival_curve, H_all_jobs_from_taskset, ARR'. }
+      { move: NOTHEP => /andP [_ NZ].
+        move: (H_valid_job_cost j' ARR'); rewrite /valid_job_cost.
+        by lia. } }
+    { move: NOTHEP => /andP [/norP [NOTHP NOTEP] JCOST].
+      rewrite ?andbT.
+      move: H_job_of_tsk; rewrite /job_of_task => /eqP <-.
+      case: (boolP (hep_task (job_task j') (job_task j))) => NOTHEP_Tsk'.
+      { rewrite /hp_task NOTHEP_Tsk' => //=.
+        rewrite andbF orFb /ep_task.
+        rewrite not_hp_hep_task in NOTHP => //.
+        rewrite NOTHP NOTHEP_Tsk' //=.
+        rewrite NOTHEP_Tsk' Bool.andb_true_l /hep_job /GEL /job_priority_point -ltNge in NOTEP.
+        have LT: ((job_arrival j)%:R + task_priority_point (job_task j)
+                < (t1)%:R + task_priority_point (job_task j'))%R by lia.
+        rewrite natrB; first by lia.
+        move: BUSY; rewrite /busy_interval_prefix.
+        move=> [? [? [? J_ARR]]].
+        by lia. }
+      { rewrite not_hep_hp_task in NOTHEP_Tsk' => //.
+        by rewrite NOTHEP_Tsk'. } }
+  Qed.
+
+End MaxNPSegmentIsBounded.

analysis/facts/blocking_bound/fp.v

+Require Export prosa.analysis.definitions.blocking_bound.fp.
+Require Export prosa.analysis.facts.busy_interval.pi.
+
+
+(** * Lower-Priority Non-Preemptive Segment is Bounded *)
+(** In this file, we prove that, under the FP scheduling policy, the
+    length of the maximum non-preemptive segment of a lower-priority
+    job (w.r.t. a job of a task [tsk]) is bounded by
+    [blocking_bound]. *)
+Section  MaxNPSegmentIsBounded.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of processor state model. *)
+  Context `{PState : ProcessorState Job}.
+
+  (** Consider an FP policy. *)
+  Context {FP : FP_policy Task}.
+
+  (** Consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** In addition, we assume the existence of a function mapping jobs
+      to their preemption points ... *)
+  Context `{JobPreemptable Job}.
+
+  (** ... and assume that it defines a valid preemption model with
+      bounded non-preemptive segments. *)
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Consider an arbitrary task set [ts], ... *)
+  Variable ts : list Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** ... and let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider any job [j] of [tsk]. *)
+  Variable j : Job.
+  Hypothesis H_job_of_tsk : job_of_task tsk j.
+
+  (** Then, the maximum length of a nonpreemptive segment among all
+      lower-priority jobs (w.r.t. the given job [j]) arrived so far is
+      bounded by [blocking_bound]. *)
+  Lemma nonpreemptive_segments_bounded_by_blocking :
+    forall t,
+      max_lp_nonpreemptive_segment arr_seq j t <= blocking_bound ts tsk.
+  Proof.
+    move=> t; move: H_job_of_tsk => /eqP TSK.
+    apply: leq_trans; first exact: max_np_job_segment_bounded_by_max_np_task_segment.
+    apply: (@leq_trans (\max_(j_lp <- arrivals_between arr_seq 0 t
+                             | (~~ hep_task (job_task j_lp) tsk) && (0 < job_cost j_lp))
+                         (task_max_nonpreemptive_segment (job_task j_lp) - ε))).
+    { rewrite /hep_job /FP_to_JLFP TSK.
+      apply: leq_big_max => j' JINB NOTHEP.
+      by rewrite leq_sub2r //. }
+    { apply /bigmax_leq_seqP => j' JINB /andP[NOTHEP POS].
+      apply leq_bigmax_cond_seq with
+        (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1);
+        last by done.
+      apply: H_all_jobs_from_taskset.
+      by apply: in_arrivals_implies_arrived (JINB). }
+  Qed.
+
+End MaxNPSegmentIsBounded.

analysis/facts/busy_interval/all.v

+Require Export prosa.analysis.facts.busy_interval.arrival.
+Require Export prosa.analysis.facts.busy_interval.carry_in.
+Require Export prosa.analysis.facts.busy_interval.quiet_time.
+Require Export prosa.analysis.facts.busy_interval.existence.
+Require Export prosa.analysis.facts.busy_interval.hep_at_pt.
+Require Export prosa.analysis.facts.busy_interval.pi_bound.
+

analysis/facts/busy_interval/arrival.v

+Require Export prosa.analysis.definitions.busy_interval.classical.
+
+(** In this module we collect some basic facts about arrival times in busy
+    windows. These are primarily useful for proof automation. *)
+
+Section Facts.
+
+  (** Consider any kind of jobs... *)
+  Context {Job : JobType} `{JobArrival Job} `{JobCost Job}.
+  (** ... and a [JLFP] policy defined on these jobs. *)
+  Context `{JLFP_policy Job}.
+  (** Consider any processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any schedule and arrival sequence. *)
+  Variable sched : schedule PState.
+  Variable arr_seq : arrival_sequence Job.
+
+  (** We note the trivial fact that, by definition, a job arrives after the
+      beginning of its busy-interval prefix ... *)
+  Fact busy_interval_prefix_job_arrival :
+    forall j t t',
+      busy_interval_prefix arr_seq sched j t t' ->
+      t <= job_arrival j.
+  Proof. by move=> ? ? ? [_ [_ [_ /andP [GEQ _]]]]. Qed.
+
+  (** ... and hence also after the beginning of its busy interval. *)
+  Fact busy_interval_job_arrival :
+    forall j t t',
+      busy_interval arr_seq sched j t t' ->
+      t <= job_arrival j.
+  Proof.
+    move=> ? ? ? [PREFIX _].
+    by eauto using busy_interval_prefix_job_arrival.
+  Qed.
+
+End Facts.
+
+(** We add the above facts into the "Hint Database" basic_rt_facts, so Coq will
+    be able to apply them automatically where needed. *)
+Global Hint Resolve
+  busy_interval_prefix_job_arrival
+  busy_interval_job_arrival
+  : basic_rt_facts.

analysis/facts/busy_interval/carry_in.v

+Require Export prosa.analysis.facts.model.workload.
+Require Export prosa.analysis.facts.model.ideal.service_of_jobs.
+Require Export prosa.analysis.facts.busy_interval.quiet_time.
+Require Export prosa.analysis.facts.busy_interval.existence.
+Require Export prosa.analysis.definitions.work_bearing_readiness.
+Require Export prosa.model.schedule.work_conserving.
+Require Export prosa.util.tactics.
+
+(** * Busy Interval From Workload Bound *)
+
+(** In the following, we derive an alternative condition for the existence of a
+    busy interval based on the total workload. If the total workload generated
+    by the task set is bounded, then there necessarily exists a moment without
+    any carry-in workload, from which it follows that a busy interval has ended. *)
+Section BusyIntervalExistence.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.
+
+  (** Allow for any fully-consuming uniprocessor model. *)
+  Context {PState : ProcessorState Job}.
+  Hypothesis H_uniproc : uniprocessor_model PState.
+  Hypothesis H_fully_consuming_proc_model : fully_consuming_proc_model PState.
+
+  (** Next, consider any schedule of the arrival sequence ... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence:
+    jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival or after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Assume a given reflexive JLFP policy. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
+
+  (** Further, allow for any work-bearing notion of job readiness ... *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** ... and assume that the schedule is work-conserving. *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** ** Times without Carry-In *)
+
+  (** As the first step, we derive a sufficient condition for the existence of a
+      no-carry-in instant for uniprocessor for JLFP schedulers. *)
+
+  (** We start by noting that, trivially, the processor has no carry-in at the
+      beginning (i.e., has no carry-in at time instant [0]). *)
+  Lemma no_carry_in_at_zero :
+    no_carry_in arr_seq sched 0.
+  Proof. by move=> j _ +; rewrite /arrived_before ltn0. Qed.
+
+  (** Next, we relate idle times to the no-carry-in condition. First, the
+      presence of a pending job implies that the processor isn't idle due to
+      work-conservation. *)
+  Lemma pending_job_not_idle :
+    forall j t,
+      arrives_in arr_seq j ->
+      pending sched j t ->
+      ~ is_idle arr_seq sched t.
+  Proof.
+    move=> j t ARR PEND IDLE.
+    have [jhp [ARRhp [READYhp _]]] :
+      exists j_hp : Job, arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
+      by apply: H_job_ready.
+    move: IDLE; rewrite is_idle_iff => /eqP; rewrite scheduled_job_at_none => // IDLE.
+    have [j_other SCHED]:  exists j_other : Job, scheduled_at sched j_other t
+      by apply: H_work_conserving ARRhp _; apply/andP.
+    by move: (IDLE j_other) => /negP.
+  Qed.
+
+  (** Second, an idle time implies no carry in at this time instant. *)
+  Lemma idle_instant_no_carry_in :
+    forall t,
+      is_idle arr_seq sched t ->
+      no_carry_in arr_seq sched t.
+  Proof.
+    move=> t IDLE j ARR HA.
+    apply/negPn/negP =>  NCOMP.
+    apply: (pending_job_not_idle j t) => //.
+    by apply/andP; split; rewrite // /has_arrived ltnW.
+  Qed.
+
+  (** Moreover, an idle time implies no carry in at the next time instant, too. *)
+  Lemma idle_instant_next_no_carry_in :
+    forall t,
+      is_idle arr_seq sched t ->
+      no_carry_in arr_seq sched t.+1.
+  Proof.
+    move=> t IDLE j ARR HA.
+    apply/negPn/negP => NCOMP.
+    apply: (pending_job_not_idle j t) => //.
+    apply/andP; split; rewrite // /has_arrived.
+    by apply: incompletion_monotonic NCOMP.
+  Qed.
+
+  (** ** Bounded-Workload Assumption *)
+
+  (** We now introduce the central assumption from which we deduce the existence
+      of a busy interval. *)
+
+  (** To this end, recall the notion of the total service of all jobs within
+      some time interval <<[t1, t2)>>. *)
+  Let total_service t1 t2 :=
+    service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2.
+
+  (** We assume that, for some positive [Δ], the sum of the total
+      blackout and the total workload generated in any interval of
+      length [Δ] starting with no carry-in is bounded by [Δ]. Note
+      that this assumption bounds the total workload of jobs released
+      in a time interval <<[t, t + Δ)>> regardless of their
+      priorities. *)
+  Variable Δ : duration.
+  Hypothesis H_delta_positive : Δ > 0.
+  Hypothesis H_workload_is_bounded :
+    forall t,
+      no_carry_in arr_seq sched t ->
+      blackout_during sched t (t + Δ) + total_workload_between arr_seq t (t + Δ) <= Δ.
+
+  (** In the following, we also require a unit-speed processor. *)
+  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
+
+  (** ** Existence of a No-Carry-In Instant *)
+
+  (** Next we prove that, if for any time instant [t] there is a point where the
+      total workload generated since [t] is upper-bounded by the length of the
+      interval, there must exist a no-carry-in instant. *)
+  Section ProcessorIsNotTooBusy.
+
+    (** As a stepping stone, we prove in the following section that for any time
+        instant [t] there exists another time instant <<t' ∈ (t, t + Δ]>> such
+        that the processor has no carry-in at time [t']. *)
+    Section ProcessorIsNotTooBusyInduction.
+
+      (** Consider an arbitrary time instant [t] ... *)
+      Variable t : duration.
+
+      (** ... such that there is no carry-in at time [t]. *)
+      Hypothesis H_no_carry_in : no_carry_in arr_seq sched t.
+
+      (** First, recall that the total service is bounded by the total
+          workload. Therefore the sum of the total blackout and the
+          total service of jobs in the interval <<[t, t + Δ)>> is
+          bounded by [Δ]. *)
+      Lemma total_service_is_bounded_by_Δ :
+        blackout_during sched t (t + Δ) + total_service t (t + Δ) <= Δ.
+      Proof.
+        have EQ: \sum_(t <= x < t + Δ) 1 = Δ.
+        { by rewrite big_const_nat iter_addn mul1n addn0 -{2}[t]addn0 subnDl subn0. }
+        rewrite -{3}EQ {EQ}.
+        rewrite /total_service /blackout_during /supply.blackout_during.
+        rewrite /service_of_jobs/service_during/service_at exchange_big //=.
+        rewrite -big_split //= leq_sum //; move => t' _.
+        have [BL|SUP] := blackout_or_supply sched t'.
+        { rewrite -[1]addn0; apply leq_add; first by case: (is_blackout).
+          rewrite leqn0; apply/eqP; apply big1 => j _.
+          eapply no_service_during_blackout in BL.
+          by apply: BL. }
+        { rewrite /is_blackout SUP add0n.
+          exact: service_of_jobs_le_1. }
+      Qed.
+
+      (** Next we consider two cases:
+          (1) The case when the sum of blackout and service is strictly less than [Δ], and
+          (2) the case when the sum of blackout and service is equal to [Δ]. *)
+
+      (** In the first case, we use the pigeonhole principle to
+          conclude that there is an idle time instant; which in turn
+          implies existence of a time instant with no carry-in. *)
+      Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
+        blackout_during sched t (t + Δ) + total_service t (t + Δ) < Δ ->
+        exists δ,
+          δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ).
+      Proof.
+        rewrite /total_service-{3}[Δ]addn0 -{2}(subnn t) addnBA // [Δ + t]addnC => LTS.
+        have [t_idle [/andP [LEt GTe] IDLE]]: exists t0 : nat,
+                                                t <= t0 < t + Δ
+                                                /\ is_idle arr_seq sched t0.
+        { apply: low_service_implies_existence_of_idle_time_rs =>//.
+          rewrite !subnKC in LTS; try by apply leq_addr.
+          by rewrite addKn. }
+        move: LEt; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
+        { exists 0; split => //.
+          rewrite addn0 EQ => s ARR BEF.
+          by apply: idle_instant_next_no_carry_in. }
+        have EX: exists γ, t_idle = t + γ.
+        { by exists (t_idle - t); rewrite subnKC // ltnW. }
+        move: EX => [γ EQ].
+        move : GTe LT; rewrite EQ ltn_add2l -{1}[t]addn0 ltn_add2l => GTe LT.
+        exists (γ.-1); split.
+        - apply leq_trans with γ.
+          + by rewrite prednK.
+          + by rewrite ltnW.
+        - rewrite -subn1 -addn1 -addnA subnKC // => s ARR BEF.
+          exact: idle_instant_no_carry_in.
+      Qed.
+
+      (** In the second case, the sum of blackout and service within
+          the time interval <<[t, t + Δ)>> is equal to [Δ]. We also
+          know that the total workload is lower-bounded by the total
+          service and upper-bounded by [Δ]. Therefore, the total
+          workload is equal to the total service, which implies
+          completion of all jobs by time [t + Δ] and hence no carry-in
+          at time [t + Δ]. *)
+      Lemma completion_of_all_jobs_implies_no_carry_in :
+        blackout_during sched t (t + Δ) + total_service t (t + Δ) = Δ ->
+        no_carry_in arr_seq sched (t + Δ).
+      Proof.
+        rewrite /total_service => EQserv s ARR BEF.
+        move: (H_workload_is_bounded t) => WORK.
+        have EQ: total_workload_between arr_seq 0 (t + Δ)
+                 = service_of_jobs sched predT (arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ);
+          last exact: workload_eq_service_impl_all_jobs_have_completed.
+        have CONSIST: consistent_arrival_times arr_seq by [].
+        have COMPL := all_jobs_have_completed_impl_workload_eq_service
+                        _ arr_seq CONSIST sched
+                        H_jobs_must_arrive_to_execute
+                        H_completed_jobs_dont_execute
+                        predT 0 t t.
+        feed_n 2 COMPL => //.
+        { move=> j A B; apply: H_no_carry_in.
+          - apply: in_arrivals_implies_arrived =>//.
+          - by have : arrived_between j 0 t
+                        by apply: (in_arrivals_implies_arrived_between arr_seq). }
+        apply/eqP; rewrite eqn_leq; apply/andP; split;
+          last by apply: service_of_jobs_le_workload.
+        rewrite /total_workload_between/total_workload (workload_of_jobs_cat arr_seq t);
+          last by apply/andP; split; [|rewrite leq_addr].
+        - rewrite (service_of_jobs_cat_scheduling_interval _ _ _ _ _ _ _ t) //;
+            last by apply/andP; split; [|rewrite leq_addr].
+          + rewrite COMPL -addnA leq_add2l.
+            rewrite -service_of_jobs_cat_arrival_interval;
+              last by apply/andP; split; [|rewrite leq_addr].
+            by evar (b : nat); rewrite -(leq_add2l b) EQserv.
+      Qed.
+
+    End ProcessorIsNotTooBusyInduction.
+
+    (** Finally, we show that any interval of length [Δ] contains a time instant
+        with no carry-in. *)
+    Lemma processor_is_not_too_busy :
+      forall t, exists δ,
+        δ < Δ /\ no_carry_in arr_seq sched (t + δ).
+    Proof.
+      elim=> [|t [δ [LE FQT]]];
+        first by exists 0; split; [ | rewrite addn0; apply: no_carry_in_at_zero].
+      move: (posnP δ) => [Z|POS]; last first.
+      - exists (δ.-1); split.
+        + by apply: leq_trans LE; rewrite prednK.
+        + by rewrite -subn1 -addn1 -addnA subnKC //.
+      - move: FQT; rewrite Z addn0 => FQT {LE}.
+        move: (total_service_is_bounded_by_Δ t); rewrite leq_eqVlt => /orP [/eqP EQ | LT].
+        + exists (Δ.-1); split; first by rewrite prednK.
+          rewrite addSn -subn1 -addn1 -addnA subnK //.
+          by apply: completion_of_all_jobs_implies_no_carry_in.
+        + by apply:low_total_service_implies_existence_of_time_with_no_carry_in.
+    Qed.
+
+  End ProcessorIsNotTooBusy.
+
+  (** ** Busy Interval Existence *)
+
+  (** Consider an arbitrary job [j] with positive cost. *)
+  Variable j : Job.
+  Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
+  Hypothesis H_job_cost_positive : job_cost_positive j.
+
+  (** We show that there must exist a busy interval <<[t1, t2)>> that
+      contains the arrival time of [j]. *)
+  Theorem busy_interval_from_total_workload_bound :
+    exists t1 t2,
+      t1 <= job_arrival j < t2
+      /\ t2 <= t1 + Δ
+      /\ busy_interval arr_seq sched j t1 t2.
+  Proof.
+    rename H_from_arrival_sequence into ARR, H_job_cost_positive into POS.
+    edestruct (exists_busy_interval_prefix
+                 arr_seq H_valid_arr_seq
+                 sched j ARR H_priority_is_reflexive (job_arrival j))
+      as [t1 [PREFIX GE]]; first by apply: job_pending_at_arrival.
+    move: GE => /andP [GE1 _].
+    exists t1.
+    have [δ [LE nCAR]]: exists δ : nat, δ < Δ /\ no_carry_in arr_seq sched (t1.+1 + δ)
+      by apply: processor_is_not_too_busy => //.
+    have QT : quiet_time arr_seq sched j (t1.+1 + δ) by apply: no_carry_in_implies_quiet_time.
+    have EX: exists t2, ((t1 < t2 <= t1.+1 + δ) && quiet_time_dec arr_seq sched j t2).
+    { exists (t1.+1 + δ); apply/andP; split.
+      - by apply/andP; split; first rewrite addSn ltnS leq_addr.
+      - exact/quiet_time_P. }
+    move: (ex_minnP EX) => [t2 /andP [/andP [GTt2 LEt2] QUIET] MIN]; clear EX.
+    have NEQ: t1 <= job_arrival j < t2.
+    { apply/andP; split=> [//|].
+      rewrite ltnNge; apply/negP => CONTR.
+      have [_ [_ [NQT _]]] := PREFIX. 
+      have {}NQT := NQT t2.
+      feed NQT; first by (apply/andP; split; [|rewrite ltnS]).
+      by apply: NQT; apply/quiet_time_P. }
+    exists t2; split=> [//|]; split.
+    { by apply: (leq_trans LEt2); rewrite addSn ltn_add2l. }
+    { move: PREFIX => [_ [QTt1 [NQT _]]]; repeat split=> //; last by exact/quiet_time_P.
+      move => t /andP [GEt LTt] QTt.
+      feed (MIN t);
+        last by move: LTt; rewrite ltnNge; move => /negP LTt; apply: LTt.
+      apply/andP; split.
+      + by apply/andP; split; last (apply leq_trans with t2; [apply ltnW |]).
+      + exact/quiet_time_P. }
+  Qed.
+
+End BusyIntervalExistence.

restructuring/analysis/facts/busy_interval_exists.v → analysis/facts/busy_interval/existence.v

-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.analysis.definitions.busy_interval.
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
-
-(** Throughout the file we assume for the classic Liu & Layland model
-   of readiness without jitter and no self-suspensions, where prending
-   jobs are always ready. *)
-Require Import rt.restructuring.model.readiness.basic.
-
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.model.schedule.work_conserving.
+Require Export prosa.analysis.definitions.job_properties.
+Require Export prosa.analysis.facts.model.service_of_jobs.
+Require Export prosa.analysis.definitions.work_bearing_readiness.
+Require Export prosa.analysis.facts.priority.inversion.
 
 (** * Existence of Busy Interval for JLFP-models *)
 (** In this module we derive a sufficient condition for existence of
-    busy intervals for uniprocessor for JLFP schedulers. *)
+    busy intervals for uni-processor for JLFP schedulers. *)
 Section ExistsBusyIntervalJLFP.
-  
+
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
 
   (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
-  Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.    
+  Context {JobTask : JobTask Job Task}.
+  Context {Arrival: JobArrival Job}.
+  Context {Cost : JobCost Job}.
 
-  (** Consider any arrival sequence with consistent arrivals. *)
+  (** Consider any valid arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
-  Variable sched : schedule (ideal.processor_state Job).
+  Hypothesis H_valid_arrival_time : valid_arrival_sequence arr_seq.
+
+  (** Next, consider any schedule of this arrival sequence ... *)
+  Context {PState : ProcessorState Job}.
+  Variable sched : schedule PState.
   Hypothesis H_jobs_come_from_arrival_sequence:
     jobs_come_from_arrival_sequence sched arr_seq.
-  
+
   (** ... where jobs do not execute before their arrival or after completion. *)
   Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
   Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Assume a given JLFP policy. *)
-  Variable higher_eq_priority : JLFP_policy Job. 
-  
+  Context {JLFP : JLFP_policy Job}.
+
+  (** Further, allow for any work-bearing notion of job readiness. *)
+  Context `{@JobReady Job PState Cost Arrival}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
   (** For simplicity, let's define some local names. *)
   Let job_pending_at := pending sched.
   Let job_completed_by := completed_by sched.
-  Let arrivals_between := arrivals_between arr_seq.
-  
+
   (** Consider an arbitrary task [tsk]. *)
   Variable tsk : Task.
 
@@ -59,63 +52,62 @@ Section ExistsBusyIntervalJLFP.
   Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
   Hypothesis H_job_task : job_of_task tsk j.
   Hypothesis H_job_cost_positive : job_cost_positive j.
-  
+
   (** Recall the list of jobs that arrive in any interval. *)
-  Let quiet_time t1 := quiet_time arr_seq sched higher_eq_priority j t1.
-  Let quiet_time_dec t1 := quiet_time_dec arr_seq sched higher_eq_priority j t1.
-  Let busy_interval_prefix t1 t2 := busy_interval_prefix arr_seq sched higher_eq_priority j t1 t2.
-  Let busy_interval t1 t2 := busy_interval arr_seq sched higher_eq_priority j t1 t2.
-  Let is_priority_inversion_bounded_by K := priority_inversion_of_job_is_bounded_by arr_seq sched higher_eq_priority j K.
-  
-  (** We begin by proving a basic lemma about completion of the job within its busy interval. *)
-  Section BasicLemma.
+  Let quiet_time t1 := quiet_time arr_seq sched j t1.
+  Let quiet_time_dec t1 := quiet_time_dec arr_seq sched j t1.
+  Let busy_interval_prefix t1 t2 := busy_interval_prefix arr_seq sched j t1 t2.
+  Let busy_interval t1 t2 := busy_interval arr_seq sched j t1 t2.
+  Let is_priority_inversion_bounded_by K := priority_inversion_of_job_is_bounded_by arr_seq sched j K.
+
+  (** We begin by proving a few basic lemmas about busy intervals. *)
+  Section BasicLemmas.
 
     (** Assume that the priority relation is reflexive. *)
-    Hypothesis H_priority_is_reflexive : reflexive_priorities.
+    Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
 
-    (** Consider any busy interval [t1, t2) of job [j]. *)
+    (** Consider any busy interval <<[t1, t2)>> of job [j]. *)
     Variable t1 t2 : instant.
     Hypothesis H_busy_interval : busy_interval t1 t2.
-    
-    (** We prove that job j completes by the end of the busy interval. *)
-    Lemma job_completes_within_busy_interval: 
+
+    (** We prove that job [j] completes by the end of the busy interval. *)
+    Lemma job_completes_within_busy_interval:
       job_completed_by j t2.
     Proof.
       rename H_priority_is_reflexive into REFL, H_busy_interval into BUSY.
       move: BUSY => [[_ [_ [_ /andP [_ ARR]]]] QUIET].
-      apply QUIET; try done.
-      apply (REFL 0).
+      exact: QUIET.
     Qed.
 
-  End BasicLemma.
-  
+  End BasicLemmas.
+
   (** In this section, we prove that during a busy interval there
-         always exists a pending job. *)
+      always exists a pending job. *)
   Section ExistsPendingJob.
-    
-    (** Let [[t1, t2]] be any interval where time t1 is quiet and time t2 is not quiet. *)
+
+    (** Let <<[t1, t2]>> be any interval where time [t1] is quiet and time [t2] is not quiet. *)
     Variable t1 t2 : instant.
     Hypothesis H_interval : t1 <= t2.
     Hypothesis H_quiet : quiet_time t1.
     Hypothesis H_not_quiet : ~ quiet_time t2.
-    
-    (** Then, we prove that there is a job pending at time t2
-         that has higher or equal priority (with respect of tsk). *)
+
+    (** Then, we prove that there is a job pending at time [t2]
+        that has higher or equal priority (with respect to [tsk]). *)
     Lemma not_quiet_implies_exists_pending_job:
       exists j_hp,
         arrives_in arr_seq j_hp /\
         arrived_between j_hp t1 t2 /\
-        higher_eq_priority j_hp j /\
-        ~ job_completed_by j_hp t2. 
+        hep_job j_hp j /\
+        ~ job_completed_by j_hp t2.
     Proof.
       rename H_quiet into QUIET, H_not_quiet into NOTQUIET.
-      destruct (has (fun j_hp => (~~ job_completed_by j_hp t2) && higher_eq_priority j_hp j)
-                    (arrivals_between t1 t2)) eqn:COMP.
+      destruct (has (fun j_hp => (~~ job_completed_by j_hp t2) && hep_job j_hp j)
+                    (arrivals_between arr_seq t1 t2)) eqn:COMP.
       { move: COMP => /hasP [j_hp ARR /andP [NOTCOMP HP]].
         move: (ARR) => INarr.
-        apply in_arrivals_implies_arrived_between in ARR; last by done.
+        apply in_arrivals_implies_arrived_between in ARR => [|//].
         apply in_arrivals_implies_arrived in INarr.
-          by exists j_hp; repeat split; last by apply/negP.
+        by exists j_hp; repeat split; last by apply/negP.
       }
       {
         apply negbT in COMP; rewrite -all_predC in COMP.
@@ -124,82 +116,79 @@ Section ExistsBusyIntervalJLFP.
         destruct (ltnP (job_arrival j_hp) t1) as [BEFORE | AFTER];
           first by specialize (QUIET j_hp IN HP BEFORE); apply completion_monotonic with (t := t1).
         feed (COMP j_hp).
-          by eapply arrived_between_implies_in_arrivals; eauto 1; apply/andP; split.
-            by rewrite /= HP andbT negbK in COMP.
+        { by apply: arrived_between_implies_in_arrivals => //;  apply/andP; split. }
+        by rewrite /= HP andbT negbK in COMP.
       }
     Qed.
 
   End ExistsPendingJob.
-  
+
   (** In this section, we prove that during a busy interval the
-         processor is never idle. *)
+      processor is never idle. *)
   Section ProcessorAlwaysBusy.
 
     (** Assume that the schedule is work-conserving ... *)
     Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
     (** ... and the priority relation is reflexive and transitive. *)
-    Hypothesis H_priority_is_reflexive : reflexive_priorities. 
-    Hypothesis H_priority_is_transitive : transitive_priorities.
-    
-    (** Consider any busy interval prefix [t1, t2). *)
+    Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
+    Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
+
+    (** Consider any busy interval prefix <<[t1, t2)>>. *)
     Variable t1 t2 : instant.
     Hypothesis H_busy_interval_prefix : busy_interval_prefix t1 t2.
 
-    (** We prove that if the processot is idle at a time instant t, then 
-           the next time instant [t+1] will be a quiet time. *)
+    (** We prove that if the processor is idle at a time instant [t],
+        then the next time instant [t+1] will be a quiet time. *)
     Lemma idle_time_implies_quiet_time_at_the_next_time_instant:
       forall (t : instant),
-        is_idle sched t ->
+        is_idle arr_seq sched t ->
         quiet_time t.+1.
     Proof.
       intros t IDLE jhp ARR HP AB.
       apply negbNE; apply/negP; intros NCOMP.
-      rewrite /arrived_before ltnS in AB.
-      move:(H_work_conserving _ t ARR) => WC.
-      feed WC.
-      { apply/andP. split.
-        - apply/negPn/negP; rewrite negb_and; intros COMP.
-          move: COMP => /orP; rewrite Bool.negb_involutive; move => [/negP CON|COM]; auto.
-          move: NCOMP => /negP NCOMP; apply: NCOMP.
-            by apply completion_monotonic with t.
-        - by move: IDLE => /eqP IDLE; rewrite /scheduled_at scheduled_in_def IDLE. 
-      }
-      move: IDLE WC => /eqP IDLE [jo SCHED].
-        by rewrite scheduled_at_def IDLE in SCHED.
+      have PEND : job_pending_at jhp t.
+      { apply/andP; split=> [//|].
+        by move: NCOMP; apply contra, completion_monotonic. }
+      apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
+      move:(H_work_conserving j' t) => WC.
+      feed_n 2 WC => [//||].
+      { apply/andP; split=> [//|].
+        exact: not_scheduled_when_idle. }
+      move: WC => [jo +]; apply/negP.
+      exact: not_scheduled_when_idle.
     Qed.
 
-    (** Next, we prove that at any time instant t within the busy interval there exists a job 
-           [jhp] such that (1) job [jhp] is pending at time [t] and (2) job [jhp] has higher-or-equal
-           priority than task [tsk]. *)
+    (** Next, we prove that at any time instant [t] within the busy interval there exists a job
+        [jhp] such that (1) job [jhp] is pending at time [t] and (2) job [jhp] has higher-or-equal
+        priority than task [tsk]. *)
     Lemma pending_hp_job_exists:
       forall t,
         t1 <= t < t2 ->
         exists jhp,
           arrives_in arr_seq jhp /\
           job_pending_at jhp t /\
-          higher_eq_priority jhp j.
+          hep_job jhp j.
     Proof.
       move => t /andP [GE LT]; move: (H_busy_interval_prefix) => [_ [QTt [NQT REL]]].
       move: (ltngtP t1.+1 t2) => [GT|CONTR|EQ]; first last.
       - subst t2; rewrite ltnS in LT.
         have EQ: t1 = t by apply/eqP; rewrite eqn_leq; apply/andP; split.
         subst t1; clear GE LT.
-        exists j; repeat split; try done.
+        exists j; repeat split=> //.
         + move: REL; rewrite ltnS -eqn_leq eq_sym; move => /eqP REL.
             by rewrite -REL; eapply job_pending_at_arrival; eauto 2.
-        + by apply (H_priority_is_reflexive 0).
       - by exfalso; move_neq_down CONTR; eapply leq_ltn_trans; eauto 2.
       - have EX: exists hp__seq: seq Job,
-        forall j__hp, j__hp \in hp__seq <-> arrives_in arr_seq j__hp /\ job_pending_at j__hp t /\ higher_eq_priority j__hp j.
-        { exists (filter (fun jo => (job_pending_at jo t) && (higher_eq_priority jo j)) (arrivals_between 0 t.+1)).
+        forall j__hp, j__hp \in hp__seq <-> arrives_in arr_seq j__hp /\ job_pending_at j__hp t /\ hep_job j__hp j.
+        { exists (filter (fun jo => (job_pending_at jo t) && (hep_job jo j)) (arrivals_between arr_seq 0 t.+1)).
           intros; split; intros T.
           - move: T; rewrite mem_filter; move => /andP [/andP [PEN HP] IN].
             repeat split; eauto using in_arrivals_implies_arrived.
           - move: T => [ARR [PEN HP]].
-            rewrite mem_filter; apply/andP; split; first (apply/andP; split); try done.
-            eapply arrived_between_implies_in_arrivals; try done.
-              by apply/andP; split; last rewrite ltnS; move: PEN => /andP [T _].
+            rewrite mem_filter; apply/andP; split; first (apply/andP; split=> //).
+            apply: arrived_between_implies_in_arrivals => //.
+            by apply/andP; split; last rewrite ltnS; move: PEN => /andP [T _].
         } move: EX => [hp__seq SE]; case FL: (hp__seq) => [ | jhp jhps].
         + subst hp__seq; exfalso.
           move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| GE].
@@ -207,37 +196,36 @@ Section ExistsBusyIntervalJLFP.
             apply NQT with t1.+1; first by apply/andP; split.
             intros jhp ARR HP ARRB; apply negbNE; apply/negP; intros NCOMP.
             move: (SE jhp) => [_ SE2].
-            rewrite in_nil in SE2; feed SE2; [clear SE2 | by done].
-            repeat split; try done; first apply/andP; split; try done.
+            rewrite in_nil in SE2; feed SE2=> [|//]; clear SE2.
+            repeat split=> //; first apply/andP; split=> //.
             apply/negP; intros COMLP.
             move: NCOMP => /negP NCOMP; apply: NCOMP.
-              by apply completion_monotonic with t1.
+            by apply completion_monotonic with t1.
           * apply NQT with t; first by apply/andP; split.
             intros jhp ARR HP ARRB; apply negbNE; apply/negP; intros NCOMP.
             move: (SE jhp) => [_ SE2].
-            rewrite in_nil in SE2; feed SE2; [clear SE2 | by done].
-              by repeat split; auto; apply/andP; split; first apply ltnW.
+            rewrite in_nil in SE2; feed SE2 => [|//]; clear SE2.
+            by repeat split; auto; apply/andP; split; first apply ltnW.
         + move: (SE jhp)=> [SE1 _]; subst; clear SE.
-            by exists jhp; apply SE1; rewrite in_cons; apply/orP; left.
+          by exists jhp; apply SE1; rewrite in_cons; apply/orP; left.
     Qed.
-    
-    (** We prove that at any time instant [t] within [t1, t2) the processor is not idle. *)
+
+    (** We prove that at any time instant [t] within <<[t1, t2)>> the processor is not idle. *)
     Lemma not_quiet_implies_not_idle:
       forall t,
         t1 <= t < t2 ->
-        ~ is_idle sched t.
+        ~ is_idle arr_seq sched t.
     Proof.
       intros t NEQ IDLE.
       move: (pending_hp_job_exists _ NEQ) => [jhp [ARR [PEND HP]]].
-      unfold work_conserving in *.
-      feed (H_work_conserving _ t ARR).
-      apply/andP; split; first by done.
-      move: IDLE => /eqP IDLE; rewrite scheduled_at_def IDLE; by done.
-      move: (H_work_conserving) => [jo SCHED].
-      move: IDLE SCHED => /eqP IDLE SCHED.
-        by rewrite scheduled_at_def IDLE in SCHED.
+      apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
+      feed (H_work_conserving _ t ARR').
+      { apply/andP; split=> [//|].
+        exact: not_scheduled_when_idle. }
+      move: (H_work_conserving) => [jo +]; apply/negP.
+      exact: not_scheduled_when_idle.
     Qed.
-    
+
   End ProcessorAlwaysBusy.
 
   (** In section we prove a few auxiliary lemmas about quiet time and service.  *)
@@ -253,96 +241,95 @@ Section ExistsBusyIntervalJLFP.
     (** Let [t1] be a quiet time. *)
     Variable t1 : instant.
     Hypothesis H_quiet_time : quiet_time t1.
-    
-    (** Assume that there is no quiet time in the interval (t1, t1 + Δ]. *)
+
+    (** Assume that there is no quiet time in the interval <<(t1, t1 + Δ]>>. *)
     Variable Δ : duration.
     Hypothesis H_no_quiet_time : forall t, t1 < t <= t1 + Δ -> ~ quiet_time t.
 
-    (** For clarity, we introduce a notion of the total service of jobs released in 
-           time interval [t_beg, t_end) during the time interval [t1, t1 + Δ). *)
+    (** For clarity, we introduce a notion of the total service of
+        jobs released in time interval <<[t_beg, t_end)>> during the
+        time interval <<[t1, t1 + Δ)>>. *)
     Let service_received_by_hep_jobs_released_during t_beg t_end :=
       service_of_higher_or_equal_priority_jobs
-        sched higher_eq_priority (arrivals_between t_beg t_end) j t1 (t1 + Δ).
+        sched (arrivals_between arr_seq t_beg t_end) j t1 (t1 + Δ).
 
     (** We prove that jobs with higher-than-or-equal priority that
-           released before time instant t1 receive no service after 
-           time instant t1. *)
+        released before time instant [t1] receive no service after time
+        instant [t1]. *)
     Lemma hep_jobs_receive_no_service_before_quiet_time:
       service_received_by_hep_jobs_released_during t1 (t1 + Δ) =
       service_received_by_hep_jobs_released_during 0 (t1 + Δ).
     Proof.
       intros.
       rewrite /service_received_by_hep_jobs_released_during
-              /service_of_higher_or_equal_priority_jobs
-              /service_of_jobs /arrivals_between.
+              /service_of_higher_or_equal_priority_jobs /service_of_jobs.
       rewrite [in X in _ = X](arrivals_between_cat _ _ t1);
-        [ | | rewrite leq_addr]; try done.
+        [ | by [] | rewrite leq_addr//].
       rewrite big_cat //=.
-      rewrite -{1}[\sum_(j <- arrivals_between _ (t1 + Δ) | _)
+      rewrite -{1}[\sum_(j <- arrivals_between arr_seq _ (t1 + Δ) | _)
                     service_during sched j t1 (t1 + Δ)]add0n.
       apply/eqP. rewrite eqn_add2r eq_sym exchange_big //=.
       rewrite big1_seq //.
       move => t' /andP [_ NEQ]; rewrite mem_iota in NEQ.
       rewrite big1_seq //.
       move => jhp /andP [HP ARR].
-      apply/eqP; rewrite eqb0. rewrite -scheduled_at_def.
+      apply: not_scheduled_implies_no_service.
       apply (completed_implies_not_scheduled _ _ H_completed_jobs_dont_execute).
-      apply completion_monotonic with t1; [ move: NEQ => /andP [T1 _] | ]; try done.
-      apply H_quiet_time; try done.
-      - by eapply in_arrivals_implies_arrived; eauto 2.
-      - by eapply in_arrivals_implies_arrived_before; eauto 2.
+      apply completion_monotonic with t1; first by move: NEQ => /andP[].
+      apply H_quiet_time => //.
+      - exact: in_arrivals_implies_arrived.
+      - exact: in_arrivals_implies_arrived_before.
     Qed.
-    
-    (** Next we prove that the total service within a "non-quiet" 
-        time interval [t1, t1 + Δ) is exactly Δ. *)
+
+    (** Next, assume that the processor is an ideal-progress, unit-speed uniprocessor. *)
+    Hypothesis H_uni : uniprocessor_model PState.
+    Hypothesis H_unit : unit_service_proc_model PState.
+    Hypothesis H_progress : ideal_progress_proc_model PState.
+
+    (** Under this assumption, we prove that the total service within a
+        "non-quiet" time interval <<[t1, t1 + Δ)>> is exactly [Δ]. *)
     Lemma no_idle_time_within_non_quiet_time_interval:
-      service_of_jobs sched predT (arrivals_between 0 (t1 + Δ)) t1 (t1 + Δ) = Δ.
+      total_service_of_jobs_in sched (arrivals_between arr_seq 0 (t1 + Δ)) t1 (t1 + Δ) = Δ.
     Proof.
-      intros; unfold service_of_jobs, service_of_higher_or_equal_priority_jobs.
+      intros; unfold total_service_of_jobs_in, service_of_jobs, service_of_higher_or_equal_priority_jobs.
       rewrite -{3}[Δ](sum_of_ones t1) exchange_big //=.
       apply/eqP; rewrite eqn_leq; apply/andP; split.
-      { rewrite leq_sum //.
-        move => t' _.
-        have SCH := service_of_jobs_le_1 sched predT (arrivals_between 0 (t1 + Δ)) _ t'. 
-          by eauto using arrivals_uniq.
-      }
-      { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=; rewrite leq_sum //.
-        move => t' /andP [/andP [LT GT] _].
-        apply/sum_seq_gt0P.
-        ideal_proc_model_sched_case_analysis_eq sched t' jo.
+      { rewrite leq_sum // => t' _.
+        have SCH := @service_of_jobs_le_1 _ _ _ _ sched predT (arrivals_between arr_seq 0 (t1 + Δ)).
+        by eapply leq_trans; [apply leqnn | apply SCH; eauto using arrivals_uniq with basic_rt_facts]. }
+      { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=
+                leq_sum // => t' /andP [/andP [LT GT] _].
+        rewrite sum_nat_gt0 filter_predT; apply/hasP.
+        have [Idle|[jo Sched_jo]] := (scheduled_at_cases _ H_valid_arrival_time sched ltac:(auto) ltac:(auto) t').
         { exfalso; move: LT; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
           { subst t'.
             feed (H_no_quiet_time t1.+1); first by apply/andP; split.
-            apply: H_no_quiet_time.
-              by apply idle_time_implies_quiet_time_at_the_next_time_instant.
-          }
+            by apply H_no_quiet_time, idle_time_implies_quiet_time_at_the_next_time_instant. }
           { feed (H_no_quiet_time t'); first by apply/andP; split; last rewrite ltnW.
             apply: H_no_quiet_time; intros j_hp IN HP ARR.
-            apply contraT; intros NOTCOMP.
-            destruct (scheduled_at sched j_hp t') eqn:SCHEDhp;
-              first by rewrite scheduled_at_def EqIdle in SCHEDhp.
-            apply negbT in SCHEDhp.
-            feed (H_work_conserving j_hp t' IN);
-              first by repeat (apply/andP; split); first by apply ltnW.
-            move: H_work_conserving => [j_other SCHEDother].
-              by rewrite scheduled_at_def EqIdle in SCHEDother.
-          }              
-        }
-        { exists jo; split.
-          - apply arrived_between_implies_in_arrivals; try done.
-            apply H_jobs_come_from_arrival_sequence with t'; try done.
-            apply/andP; split; first by done.
+            apply contraT; intros NCOMP.
+            have PEND : job_pending_at j_hp t'.
+            { apply/andP; split.
+              - by rewrite /has_arrived ltnW.
+              - by move: NCOMP; apply contra, completion_monotonic. }
+            apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
+            feed (H_work_conserving _ t' ARR').
+            { by apply/andP; split => //; apply: not_scheduled_when_idle. }
+            exfalso; move: H_work_conserving => [j_other +]; apply/negP.
+            exact: not_scheduled_when_idle. } }
+        { exists jo.
+          - apply arrived_between_implies_in_arrivals => //.
+            apply/andP; split=> [//|].
             apply H_jobs_must_arrive_to_execute in Sched_jo.
-              by apply leq_ltn_trans with t'. 
-          - by rewrite lt0b -scheduled_at_def. 
-        }
-      }
+            by apply leq_ltn_trans with t'.
+          - by apply: H_progress. } }
     Qed.
-    
+
+
   End QuietTimeAndServiceOfJobs.
 
   (** In this section, we show that the length of any busy interval
-      is bounded, as long as there is enough supply to accomodate
+      is bounded, as long as there is enough supply to accommodate
       the workload of tasks with higher or equal priority. *)
   Section BoundingBusyInterval.
 
@@ -351,37 +338,37 @@ Section ExistsBusyIntervalJLFP.
 
     (** ... and there are no duplicate job arrivals, ... *)
     Hypothesis H_arrival_sequence_is_a_set:
-      arrival_sequence_uniq arr_seq.        
+      arrival_sequence_uniq arr_seq.
 
     (** ... and the priority relation is reflexive and transitive. *)
-    Hypothesis H_priority_is_reflexive: reflexive_priorities.
-    Hypothesis H_priority_is_transitive: transitive_priorities.
-    
-    (** Next, we recall the notion of workload of all jobs released in a given interval
-           [t1, t2) that have higher-or-equal priority w.r.t the job j being analyzed. *)
+    Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
+    Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
+
+    (** Next, we recall the notion of workload of all jobs released in
+        a given interval <<[t1, t2)>> that have higher-or-equal
+        priority w.r.t. the job [j] being analyzed. *)
     Let hp_workload t1 t2 :=
-      workload_of_higher_or_equal_priority_jobs
-        higher_eq_priority j (arrivals_between t1 t2).
+      workload_of_hep_jobs arr_seq j t1 t2.
 
     (** With regard to the jobs with higher-or-equal priority that are released
-           in a given interval [t1, t2), we also recall the service received by these
-           jobs in the same interval [t1, t2). *)
+           in a given interval <<[t1, t2)>>, we also recall the service received by these
+           jobs in the same interval <<[t1, t2)>>. *)
     Let hp_service t1 t2 :=
       service_of_higher_or_equal_priority_jobs
-        sched higher_eq_priority (arrivals_between t1 t2) j t1 t2.
+        sched (arrivals_between arr_seq t1 t2) j t1 t2.
 
     (** Now we begin the proof. First, we show that the busy interval is bounded. *)
     Section BoundingBusyInterval.
 
-      (** Suppose that job j is pending at time t_busy. *)
+      (** Suppose that job [j] is pending at time [t_busy]. *)
       Variable t_busy : instant.
       Hypothesis H_j_is_pending : job_pending_at j t_busy.
-      
+
       (** First, we show that there must exist a busy interval prefix. *)
       Section LowerBound.
 
-        (** Since job j is pending, there is a (potentially unbounded)
-               busy interval that starts no later than with the arrival of j. *)
+        (** Since job [j] is pending, there is a (potentially unbounded)
+            busy interval that starts no later than with the arrival of [j]. *)
         Lemma exists_busy_interval_prefix:
           exists t1,
             busy_interval_prefix t1 t_busy.+1 /\
@@ -396,252 +383,258 @@ Section ExistsBusyIntervalJLFP.
             { intros j_hp IN HP ARR; move: PRED => /allP PRED; feed (PRED j_hp).
               - by eapply arrived_between_implies_in_arrivals; eauto.
               - by rewrite HP implyTb in PRED.
-            } 
+            }
             exists last0.
             have JAIN: last0 <= job_arrival j <= t_busy.
             { apply/andP; split; last by move: PEND => /andP [ARR _].
               move_neq_up BEFORE.
               move: PEND => /andP [_ NOTCOMP].
-              feed (QUIET j H_from_arrival_sequence); first by apply (H_priority_is_reflexive 0).
+              feed (QUIET j H_from_arrival_sequence); first by apply H_priority_is_reflexive.
               specialize (QUIET BEFORE).
-              apply completion_monotonic with (t' := t_busy) in QUIET; first by rewrite QUIET in NOTCOMP. 
+              apply completion_monotonic with (t' := t_busy) in QUIET; first by rewrite QUIET in NOTCOMP.
                 by apply bigmax_ltn_ord with (i0 := t).
             }
-            repeat split; try done.
-            + by apply bigmax_ltn_ord with (i0 := t).
-            + move => t0 /andP [GTlast LTbusy] QUIET0.
-              have PRED0: quiet_time_dec t0.
-              apply/allP; intros j_hp ARR; apply/implyP; intros HP.
-              apply QUIET0; eauto 2 using in_arrivals_implies_arrived, in_arrivals_implies_arrived_before.
-              move_neq_down GTlast.
-                by eapply (@leq_bigmax_cond _ (fun (x: 'I_t_busy.+1) => quiet_time_dec x) (fun x => x) (Ordinal LTbusy)).
-          -  apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
-             exists 0; split; last by apply/andP; split; last by move: PEND => /andP [ARR _].
-             repeat split; first by intros j_hp _ _ ARR; rewrite /arrived_before ltn0 in ARR.
-             move => t /andP [GE LT].
-             specialize (ALL (Ordinal LT)); move: ALL => /negP ALL.
-             intros QUIET; apply ALL; simpl.
-             apply/allP; intros j_hp ARR; apply/implyP; intros HP.
-             apply QUIET; eauto 2 using in_arrivals_implies_arrived, in_arrivals_implies_arrived_before.
-             apply/andP; split; first by done.
-               by move: PEND => /andP [ARR _].
-        Qed.             
+            repeat split=> //.
+            * by apply bigmax_ltn_ord with (i0 := t).
+            * move => t0 /andP [GTlast LTbusy] QUIET0.
+              have PRED0: quiet_time_dec t0 by apply/quiet_time_P.
+              move: (@leq_bigmax_cond _ (fun (x: 'I_t_busy.+1) => quiet_time_dec x) (fun x => x) (Ordinal LTbusy) PRED0) => /=.
+              by rewrite -/last0; move: GTlast; clear; lia.
+          - apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP /= ALL.
+            exists 0; split; last by apply/andP; split; last by move: PEND => /andP [ARR _].
+            repeat split; first by intros j_hp _ _ ARR; rewrite /arrived_before ltn0 in ARR.
+            * move => t /andP [GE LT] /quiet_time_P QUIET.
+              apply/negP; [exact: (ALL (Ordinal LT))|] => /=.
+              exact: QUIET.
+            * apply/andP; split=> [//|].
+              by move: PEND => /andP[].
+        Qed.
 
       End LowerBound.
-      
-      (** Next we prove that, if there is a point where the requested workload
-             is upper-bounded by the supply, then the busy interval eventually ends. *)
+
+      (** Next we prove that, if there is a point where the requested
+          workload is upper-bounded by the supply, then the busy
+          interval eventually ends. *)
       Section UpperBound.
 
-        (** Consider any busy interval prefix of job j. *)
+        (** The following proofs assume that the processor is an ideal-progress,
+            unit-speed uniprocessor. *)
+        Hypothesis H_uni : uniprocessor_model PState.
+        Hypothesis H_unit : unit_service_proc_model PState.
+        Hypothesis H_progress : ideal_progress_proc_model PState.
+
+        (** Consider any busy interval prefix of job [j]. *)
         Variable t1 : instant.
         Hypothesis H_is_busy_prefix : busy_interval_prefix t1 t_busy.+1.
-        
-        (** Let priority_inversion_bound be a constant which bounds
-             length of a priority inversion. *)
-        Variable priority_inversion_bound: instant.
-        Hypothesis H_priority_inversion_is_bounded:
+
+        (** Let's define A as the relative arrival time of job [j]
+            (with respect to time [t1]). *)
+        Let A := job_arrival j - t1.
+
+        (** Let [priority_inversion_bound] be a constant that bounds
+            the length of any priority inversion. *)
+        Variable priority_inversion_bound : instant -> instant.
+        Hypothesis H_priority_inversion_is_bounded :
           is_priority_inversion_bounded_by priority_inversion_bound.
-        
+
         (** Next, assume that for some positive delta, the sum of requested workload
-               at time [t1 + delta] and constant priority_inversion_bound is bounded by 
-               delta (i.e., the supply). *)
+            at time [t1 + delta] and constant priority_inversion_bound is bounded by
+            delta (i.e., the supply). *)
         Variable delta : duration.
         Hypothesis H_delta_positive : delta > 0.
         Hypothesis H_workload_is_bounded :
-          priority_inversion_bound + hp_workload t1 (t1 + delta) <= delta.
+          priority_inversion_bound A + hp_workload t1 (t1 + delta) <= delta.
 
-        (** If there is a quiet time by time (t1 + delta), it trivially follows that
-               the busy interval is bounded.
-               Thus, let's consider first the harder case where there is no quiet time,
-               which turns out to be impossible. *)
+        (** If there is a quiet time by time [t1 + delta], it
+            trivially follows that the busy interval is bounded.
+            Thus, let's consider first the harder case where there is
+            no quiet time, which turns out to be impossible. *)
         Section CannotBeBusyForSoLong.
-          
-          (** Assume that there is no quiet time in the interval (t1, t1 + delta]. *)
+
+          (** Assume that there is no quiet time in the interval <<(t1, t1 + delta]>>. *)
           Hypothesis H_no_quiet_time:
-            forall t, t1 < t <= t1 + delta -> ~ quiet_time t.                
-
-          (** Since the interval is always non-quiet, the processor is always busy
-                 with tasks of higher-or-equal priority or some lower priority job which was scheduled,
-                 i.e., the sum of service done by jobs with actual arrival time in [t1, t1 + delta) 
-                 and priority inversion equals delta. *)
-          Lemma busy_interval_has_uninterrupted_service: 
-            delta <= priority_inversion_bound + hp_service t1 (t1 + delta).
-          Proof. 
+            forall t, t1 < t <= t1 + delta -> ~ quiet_time t.
+
+          (** Since the interval is always non-quiet, the processor is
+              always busy with tasks of higher-or-equal priority or
+              some lower priority job which was scheduled, i.e., the
+              sum of service done by jobs with actual arrival time in
+              <<[t1, t1 + delta)>> and priority inversion equals
+              [delta]. *)
+          Lemma busy_interval_has_uninterrupted_service:
+            delta <= priority_inversion_bound A + hp_service t1 (t1 + delta).
+          Proof.
             move: H_is_busy_prefix => [H_strictly_larger [H_quiet [_ EXj]]].
-            destruct (delta <= priority_inversion_bound) eqn:KLEΔ.
-            { by apply leq_trans with priority_inversion_bound; last rewrite leq_addr. }
-            apply negbT in KLEΔ; rewrite -ltnNge in KLEΔ. 
-            apply leq_trans with (cumulative_priority_inversion sched higher_eq_priority j t1 (t1 + delta) + hp_service t1 (t1 + delta)).
-            { rewrite /hp_service hep_jobs_receive_no_service_before_quiet_time //.
-              rewrite /service_of_higher_or_equal_priority_jobs /service_of_jobs sum_pred_diff. 
-              rewrite addnBA; last first.
-              { by rewrite big_mkcond //= leq_sum //; intros j' _; case (higher_eq_priority j' j). } 
-              rewrite addnC -addnBA.
-              { intros. have TT := no_idle_time_within_non_quiet_time_interval.
-                  by unfold service_of_jobs in TT; rewrite TT // leq_addr.
-              } 
-              { rewrite /cumulative_priority_inversion /is_priority_inversion exchange_big //=.
-                apply leq_sum_seq; move => t II _.
-                rewrite mem_index_iota in II; move: II => /andP [GEi LEt].
-                case SCHED: (sched t) => [j1 | ]; simpl; first last.
-                { rewrite leqn0 big1_seq //. }
-                { case PRIO1: (higher_eq_priority j1 j); simpl; first last.
-                  - rewrite <- SCHED.
-                    have SCH := service_of_jobs_le_1 sched _ _ _ t; eauto using arrivals_uniq. 
-                  - rewrite leqn0 big1_seq; first by done.
-                    move => j2 /andP [PRIO2 ARRj2].
-                    case EQ: (j1 == j2).
-                    + by move: EQ => /eqP EQ; subst j2; rewrite PRIO1 in PRIO2.
-                    + apply/eqP; rewrite eqb0; apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
-                        by inversion CONTR; clear CONTR; subst j2; rewrite PRIO1 in PRIO2. } } }
+            destruct (delta <= priority_inversion_bound A) eqn:KLEΔ.
+            { by apply leq_trans with (priority_inversion_bound A); last rewrite leq_addr. }
+            apply negbT in KLEΔ; rewrite -ltnNge in KLEΔ.
+            apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 (t1 + delta) + hp_service t1 (t1 + delta)).
+            { rewrite /hp_service hep_jobs_receive_no_service_before_quiet_time // /service_of_higher_or_equal_priority_jobs.
+              rewrite service_of_jobs_negate_pred // addnBA; last by apply service_of_jobs_pred_impl; eauto 2.
+              rewrite addnC -addnBA; first by rewrite no_idle_time_within_non_quiet_time_interval // leq_addr.
+              rewrite service_of_jobs_sum_over_time_interval //.
+              apply leq_sum_seq; move => t II _; rewrite mem_index_iota in II; move: II => /andP [GEi LEt].
+              have [IDLE|[j' SCHED]] := (scheduled_at_cases _ H_valid_arrival_time sched ltac:(auto) ltac:(auto) t).
+              { apply leq_trans with 0; [rewrite leqn0; apply/eqP | by apply leq0n].
+                apply: big1 => j' NHEP.
+                by apply/not_scheduled_implies_no_service/not_scheduled_when_idle. }
+              { destruct (hep_job j' j) eqn:PRIO1.
+                - rewrite service_of_jobs_nsched_or_unsat//.
+                  intros j'' IN; apply/andP; intros [NHEP SCHED''].
+                  have EQ: j'' = j' by eapply H_uni; eauto 2.
+                  by subst j''; rewrite PRIO1 in NHEP.
+                - have SCH := @service_of_jobs_le_1 _ _ _ _ _ (fun i => ~~ hep_job i j) (arrivals_between arr_seq 0 (t1 + delta)).
+                  eapply leq_trans; first by apply: SCH; eauto using arrivals_uniq with basic_rt_facts.
+                  clear SCH; rewrite lt0b; apply/andP; split.
+                  + apply/negP; intros SCHED'.
+                    have EQ : j = j'.
+                    { apply: H_uni SCHED.
+                      by rewrite -(scheduled_jobs_at_iff arr_seq). }
+                    subst; move: PRIO1 => /negP PRIO1; apply: PRIO1.
+                    apply H_priority_is_reflexive.
+                  + apply/hasP; exists j'; last by rewrite PRIO1.
+                    by rewrite scheduled_jobs_at_iff. } }
             { rewrite leq_add2r.
               destruct (t1 + delta <= t_busy.+1) eqn:NEQ; [ | apply negbT in NEQ; rewrite -ltnNge in NEQ].
-              - apply leq_trans with (cumulative_priority_inversion  sched higher_eq_priority j t1 t_busy.+1); last eauto 2.
-                  by rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + delta)) //=; rewrite leq_addr.
-              -  apply H_priority_inversion_is_bounded; repeat split; try done.
+              - apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 t_busy.+1); last eauto 2.
+                by rewrite [in X in _ <= X](cumulative_priority_inversion_cat _ _ _ (t1 + delta)) //= leq_addr.
+              -  apply H_priority_inversion_is_bounded; repeat split=> //.
                  + by rewrite -addn1 leq_add2l.
-                 + move => t' /andP [LT GT]; apply H_no_quiet_time.
-                     by apply/andP; split; [ | rewrite ltnW ].
-                 + move: EXj => /andP [T1 T2].
-                     by apply/andP; split; [done | apply ltn_trans with (t_busy.+1)].
-            }
+                 + by move => t' /andP [LT GT]; apply H_no_quiet_time; apply/andP; split; last rewrite ltnW.
+                 + by move: EXj => /andP [T1 T2]; apply/andP; split; last apply ltn_trans with (t_busy.+1). }
           Qed.
-          
-          (** Moreover, the fact that the interval is not quiet also implies
-                 that there's more workload requested than service received. *)
+
+          (** Moreover, the fact that the interval is not quiet also
+              implies that there's more workload requested than
+              service received. *)
           Lemma busy_interval_too_much_workload:
             hp_workload t1 (t1 + delta) > hp_service t1 (t1 + delta).
           Proof.
             have PEND := not_quiet_implies_exists_pending_job.
-            rename H_no_quiet_time into NOTQUIET, 
+            rename H_no_quiet_time into NOTQUIET,
             H_is_busy_prefix into PREFIX.
-            set l := arrivals_between t1 (t1 + delta).
-            set hep := higher_eq_priority.
+            set l := arrivals_between arr_seq t1 (t1 + delta).
+            set hep := hep_job.
             unfold hp_service, service_of_higher_or_equal_priority_jobs, service_of_jobs,
-            hp_workload, workload_of_higher_or_equal_priority_jobs, workload_of_jobs.
-            fold arrivals_between l hep.
+            hp_workload, workload_of_hep_jobs, workload_of_jobs.
+            fold l hep.
             move: (PREFIX) => [_ [QUIET _]].
             move: (NOTQUIET) => NOTQUIET'.
             feed (NOTQUIET' (t1 + delta)).
-            { by apply/andP; split; first
-                by rewrite -addn1 leq_add2l.
-            }
+            { by apply/andP; split; first rewrite -addn1 leq_add2l. }
             feed (PEND t1 (t1 + delta)); first by apply leq_addr.
             specialize (PEND QUIET NOTQUIET').
             move: PEND => [j0 [ARR0 [/andP [GE0 LT0] [HP0 NOTCOMP0]]]].
             have IN0: j0 \in l.
-            { by eapply arrived_between_implies_in_arrivals; eauto 1; apply/andP; split. }
+            { by apply: arrived_between_implies_in_arrivals => //; apply/andP; split. }
             have UNIQ: uniq l by eapply arrivals_uniq; eauto 1.
             rewrite big_mkcond [\sum_(_ <- _ | _ _ _)_]big_mkcond //=.
-            rewrite (bigD1_seq j0); [simpl | by done | by done].
-            rewrite (bigD1_seq j0); [simpl | by done | by done].
-            rewrite /hep HP0.
+            rewrite (bigD1_seq j0)//= (bigD1_seq j0)//= /hep HP0.
             rewrite -add1n addnA [1 + _]addnC addn1.
             apply leq_add; last first.
-            {
-              apply leq_sum; intros j1 NEQ.
-              destruct (higher_eq_priority j1 j); last by done.
-                by apply cumulative_service_le_job_cost, ideal_proc_model_provides_unit_service.
-            }
-            rewrite ignore_service_before_arrival; rewrite //; [| by apply ltnW].
-            rewrite <- ignore_service_before_arrival with (t2:=0); rewrite //; [|by apply ltnW].
-              by rewrite ltnNge; apply/negP.
-          Qed.               
-          
-          (** Using the two lemmas above, we infer that the workload is larger than the
-                 interval length. However, this contradicts the assumption H_workload_is_bounded. *)
+            { apply: leq_sum=>  j1 NEQ.
+              case: (hep_job _ _) => //.
+              by apply: cumulative_service_le_job_cost. }
+            rewrite ignore_service_before_arrival//.
+            rewrite -(ignore_service_before_arrival _ _ _ 0)//.
+            by rewrite ltnNge; apply/negP.
+          Qed.
+
+          (** Using the two lemmas above, we infer that the workload
+              is larger than the interval length. However, this
+              contradicts the assumption [H_workload_is_bounded]. *)
           Corollary busy_interval_workload_larger_than_interval:
-            priority_inversion_bound + hp_workload t1 (t1 + delta)  > delta.
+            priority_inversion_bound A + hp_workload t1 (t1 + delta) > delta.
           Proof.
-            apply leq_ltn_trans with (priority_inversion_bound + hp_service t1 (t1 + delta)).
-            apply busy_interval_has_uninterrupted_service.
-            rewrite ltn_add2l.
-            apply busy_interval_too_much_workload.
+            apply leq_ltn_trans with (priority_inversion_bound A + hp_service t1 (t1 + delta)).
+            - by apply busy_interval_has_uninterrupted_service.
+            - rewrite ltn_add2l.
+              by apply busy_interval_too_much_workload.
           Qed.
-          
-        End CannotBeBusyForSoLong.  
 
-        (** Since the interval cannot remain busy for so long, we prove that
-               the busy interval finishes at some point t2 <= t1 + delta. *)
+        End CannotBeBusyForSoLong.
+
+        (** Since the interval cannot remain busy for so long, we
+            prove that the busy interval finishes at some point [t2 <=
+            t1 + delta]. *)
         Lemma busy_interval_is_bounded:
           exists t2,
             t2 <= t1 + delta /\
             busy_interval t1 t2.
-        Proof. 
+        Proof.
           move: H_is_busy_prefix => [LT [QT [NQ NEQ]]].
           destruct ([exists t2:'I_(t1 + delta).+1, (t2 > t1) && quiet_time_dec t2]) eqn:EX.
           - have EX': exists (t2 : instant), ((t1 < t2 <= t1 + delta) && quiet_time_dec t2).
             { move: EX => /existsP [t2 /andP [LE QUIET]].
-              exists t2; apply/andP; split; last by done.
-                by apply/andP; split; last (rewrite -ltnS; apply ltn_ord). }
+              exists t2; apply/andP; split=> [|//].
+              by apply/andP; split; last (rewrite -ltnS; apply ltn_ord). }
             move: (ex_minnP EX') => [t2 /andP [/andP [GT LE] QUIET] MIN]; clear EX EX'.
-            exists t2; split; [ | split; [repeat split | ]]; try done.
-            + move => t /andP [GT1 LT2] BUG. 
+            exists t2; split; [ | split; [repeat split | ]] => //.
+            + move => t /andP [GT1 LT2] BUG.
               feed (MIN t); first (apply/andP; split).
-              * by apply/andP; split; last by apply leq_trans with (n := t2); eauto using ltnW. 
-              * apply/allP; intros j_hp ARR; apply/implyP; intro HP.
-                apply BUG; eauto 2 using in_arrivals_implies_arrived, ARR, in_arrivals_implies_arrived_before.
-                  by apply leq_ltn_trans with (p := t2) in MIN; first by rewrite ltnn in MIN.
+              * by apply/andP; split; last by apply leq_trans with (n := t2); eauto using ltnW.
+              * by apply/quiet_time_P.
+              * by apply leq_ltn_trans with (p := t2) in MIN; first by rewrite ltnn in MIN.
             + move: NEQ => /andP [IN1 IN2].
-              apply/andP; split; first by done.
+              apply/andP; split=> [//|].
               apply leq_ltn_trans with t_busy; eauto 2.
               rewrite ltnNge; apply/negP; intros CONTR.
               apply NQ with t2.
               * by apply/andP; split; last rewrite ltnS.
-              * intros jhp ARR HP AB. 
-                move: QUIET => /allP QUIET; feed (QUIET jhp).
-                eapply arrived_between_implies_in_arrivals; eauto 2.
-                  by move: QUIET => /implyP QUIET; apply QUIET.
+              * by apply/quiet_time_P.
             + intros j_hp IN HP ARR.
               move: QUIET => /allP QUIET; feed (QUIET j_hp).
               * by eapply arrived_between_implies_in_arrivals; last apply ARR.
               * by move: QUIET => /implyP QUIET; apply QUIET.
-          - apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL'.
+          - apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP /= ALL'.
             have ALL: forall t, t1 < t <= t1 + delta -> ~ quiet_time t.
             { move => t /andP [GTt LEt] QUIET; rewrite -ltnS in LEt.
-              specialize (ALL' (Ordinal LEt)); rewrite negb_and /= GTt orFb in ALL'. 
-              move: ALL' => /negP ALL'; apply ALL'; clear ALL'.
-              apply/allP; intros j_hp ARR; apply/implyP; intro HP.
-              apply QUIET; eauto 2 using in_arrivals_implies_arrived, ARR, in_arrivals_implies_arrived_before.
-            } clear ALL'; exfalso.
+              move: (ALL' (Ordinal LEt)) => /negP /=; apply.
+              by apply/andP; split => //; apply/quiet_time_P. }
+            clear ALL'; exfalso.
             have TOOMUCH := busy_interval_workload_larger_than_interval.
             have BOUNDED := H_workload_is_bounded.
-              by move: (leq_trans (TOOMUCH ALL) BOUNDED); rewrite ltnn.                  
+            by move: (leq_trans (TOOMUCH ALL) BOUNDED); rewrite ltnn.
         Qed.
-        
+
       End UpperBound.
 
     End BoundingBusyInterval.
 
-    (** In this section, we show that from a workload bound we can infer
-           the existence of a busy interval. *)
+    (** The following proofs assume that the processor is an ideal-progress,
+        unit-speed uniprocessor. *)
+    Hypothesis H_uni : uniprocessor_model PState.
+    Hypothesis H_unit : unit_service_proc_model PState.
+    Hypothesis H_progress : ideal_progress_proc_model PState.
+
+    (** In this section, we show that from a workload bound we can
+        infer the existence of a busy interval. *)
     Section BusyIntervalFromWorkloadBound.
 
-      (** Let priority_inversion_bound be a constant that bounds the length of a priority inversion. *)
-      Variable priority_inversion_bound: duration.
-      Hypothesis H_priority_inversion_is_bounded:
-        is_priority_inversion_bounded_by priority_inversion_bound.
+      (** Let [priority_inversion_bound] be a constant that bounds the
+          length of a priority inversion. *)
+      Variable priority_inversion_bound : duration -> duration.
+      Hypothesis H_priority_inversion_is_bounded :
+        is_priority_inversion_bounded_by priority_inversion_bound .
 
       (** Assume that for some positive delta, the sum of requested workload at
-             time (t1 + delta) and priority inversion is bounded by delta (i.e., the supply). *)
-      Variable delta: duration.
-      Hypothesis H_delta_positive: delta > 0.
-      Hypothesis H_workload_is_bounded:
-        forall t, priority_inversion_bound + hp_workload t (t + delta) <= delta.
+          time [t1 + delta] and priority inversion is bounded by delta (i.e., the supply). *)
+      Variable delta : duration.
+      Hypothesis H_delta_positive : delta > 0.
+      Hypothesis H_workload_is_bounded :
+        forall t, priority_inversion_bound (job_arrival j - t) + hp_workload t (t + delta) <= delta.
 
-      (** Next, we assume that job j has positive cost, from which we can
-             infer that there is a time in which j is pending. *)
-      Hypothesis H_positive_cost: job_cost j > 0.
+      (** Next, we assume that job j has positive cost, from which we
+          can infer that there is a time in which j is pending. *)
+      Hypothesis H_positive_cost : job_cost j > 0.
 
-      (** Therefore there must exists a busy interval [t1, t2) that
-             contains the arrival time of j. *)
+      (** Therefore there must exists a busy interval <<[t1, t2)>> that contains the arrival time of [j]. *)
       Corollary exists_busy_interval:
-        exists t1 t2, 
+        exists t1 t2,
           t1 <= job_arrival j < t2 /\
           t2 <= t1 + delta /\
           busy_interval t1 t2.
-      Proof. 
+      Proof.
         have PREFIX := exists_busy_interval_prefix.
         move: (H_workload_is_bounded) => WORK.
         feed (PREFIX (job_arrival j)).
@@ -653,50 +646,51 @@ Section ExistsBusyIntervalJLFP.
         }
         move: PREFIX => [t1 [PREFIX /andP [GE1 GEarr]]].
         have BOUNDED := busy_interval_is_bounded
-                          (job_arrival j) t1  PREFIX priority_inversion_bound _ delta
-                          H_delta_positive.            
-        feed_n 2 BOUNDED; try done.
+                          (job_arrival j) _ H_uni H_unit H_progress t1  PREFIX priority_inversion_bound _ delta
+                          H_delta_positive.
+        feed_n 3 BOUNDED => //.
+        { by apply job_pending_at_arrival. }
         move: BOUNDED => [t2 [GE2 BUSY]].
         exists t1, t2; split.
-        { apply/andP; split; first by done.
+        { apply/andP; split=> [//|].
           apply contraT; rewrite -leqNgt; intro BUG.
           move: BUSY PREFIX => [[LE12 _] QUIET] [_ [_ [NOTQUIET _]]].
           feed (NOTQUIET t2); first by apply/andP; split.
             by exfalso; apply NOTQUIET.
         }
-          by split. 
+        by split.
       Qed.
-      
+
     End BusyIntervalFromWorkloadBound.
 
     (** If we know that the workload is bounded, we can also use the
-           busy interval to infer a response-time bound. *)
+        busy interval to infer a response-time bound. *)
     Section ResponseTimeBoundFromBusyInterval.
 
       (** Let priority_inversion_bound be a constant that bounds the length of a priority inversion. *)
-      Variable priority_inversion_bound: duration.
+      Variable priority_inversion_bound: duration -> duration.
       Hypothesis H_priority_inversion_is_bounded:
         is_priority_inversion_bounded_by priority_inversion_bound.
 
       (** Assume that for some positive delta, the sum of requested workload at
-             time (t1 + delta) and priority inversion is bounded by delta (i.e., the supply). *)
+          time [t1 + delta] and priority inversion is bounded by delta (i.e., the supply). *)
       Variable delta: duration.
       Hypothesis H_delta_positive: delta > 0.
       Hypothesis H_workload_is_bounded:
-        forall t, priority_inversion_bound + hp_workload t (t + delta) <= delta.
+        forall t, priority_inversion_bound (job_arrival j - t) + hp_workload t (t + delta) <= delta.
 
-      (** Then, job j must complete by (job_arrival j + delta). *)
+      (** Then, job [j] must complete by [job_arrival j + delta]. *)
       Lemma busy_interval_bounds_response_time:
         job_completed_by j (job_arrival j + delta).
       Proof.
         have BUSY := exists_busy_interval priority_inversion_bound _ delta.
-        move: (posnP (@job_cost _ H2 j)) => [ZERO|POS].
+        move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
         { by rewrite /job_completed_by /completed_by ZERO. }
-        feed_n 4 BUSY; try by done.
+        feed_n 4 BUSY => //.
         move: BUSY => [t1 [t2 [/andP [GE1 LT2] [GE2 BUSY]]]].
-        apply completion_monotonic with (t := t2); try (by done);
-          first by apply leq_trans with (n := t1 + delta); [| by rewrite leq_add2r].
-        apply job_completes_within_busy_interval with (t1 := t1); try by done.
+        apply completion_monotonic with (t := t2) => //.
+          - by apply leq_trans with (n := t1 + delta); [| rewrite leq_add2r].
+          - by apply job_completes_within_busy_interval with (t1 := t1).
       Qed.
 
     End ResponseTimeBoundFromBusyInterval.

analysis/facts/busy_interval/hep_at_pt.v

+Require Export prosa.model.schedule.priority_driven.
+Require Export prosa.analysis.facts.busy_interval.existence.
+Require Export prosa.util.tactics.
+Require Export prosa.model.task.preemption.parameters.
+Require Export prosa.analysis.facts.model.preemption.
+
+(** * Processor Executes HEP jobs at Preemption Point *)
+
+(** In this file, we show that, given a busy interval of a job [j],
+    the processor is always busy scheduling a higher-or-equal-priority
+    job at any preemptive point inside the busy interval. *)
+Section ProcessorBusyWithHEPJobAtPreemptionPoints.
+
+  (** Consider any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{Arrival : JobArrival Job}.
+  Context `{Cost : JobCost Job}.
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
+
+  (** ... and any uniprocessor schedule of this arrival sequence. *)
+  Context {PState : ProcessorState Job}.
+  Hypothesis H_uni : uniprocessor_model PState.
+  Variable sched : schedule PState.
+
+  (** Consider a JLFP policy that indicates a higher-or-equal priority relation,
+      and assume that the relation is reflexive and transitive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
+  Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
+
+  (** In addition, we assume the existence of a function mapping a job
+      and its progress to a boolean value saying whether this job is
+      preemptable at its current point of execution. *)
+  Context `{JobPreemptable Job}.
+
+  (** Further, allow for any work-bearing notion of job readiness. *)
+  Context `{@JobReady Job PState Cost Arrival}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** We assume that the schedule is valid and that all jobs come from the arrival sequence. *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** Next, we assume that the schedule is a work-conserving schedule... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** ... and the schedule respects the scheduling policy at every preemption point. *)
+  Hypothesis H_respects_policy :
+    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
+
+  (** Consider any job [j] with positive job cost. *)
+  Variable j : Job.
+  Hypothesis H_j_arrives : arrives_in arr_seq j.
+  Hypothesis H_job_cost_positive : job_cost_positive j.
+
+  (** Consider any busy interval prefix <<[t1, t2)>> of job [j]. *)
+  Variable t1 t2 : instant.
+  Hypothesis H_busy_interval_prefix :
+    busy_interval_prefix arr_seq sched j t1 t2.
+
+  (** Consider an arbitrary preemption time t ∈ <<[t1,t2)>>. *)
+  Variable t : instant.
+  Hypothesis H_t_in_busy_interval : t1 <= t < t2.
+  Hypothesis H_t_preemption_time : preemption_time arr_seq sched t.
+
+  (** First note since [t] lies inside the busy interval,
+      the processor cannot be idle at time [t]. *)
+  Lemma instant_t_is_not_idle:
+    ~ is_idle arr_seq sched t.
+  Proof.
+    by move => IDLE; apply: not_quiet_implies_not_idle => //.
+  Qed.
+
+  (** Next we consider two cases:
+        (1) [t] is less than [t2 - 1] and
+        (2) [t] is equal to [t2 - 1]. *)
+
+  (** In case when [t < t2 - 1], we use the fact that time instant
+      [t+1] is not a quiet time. The later implies that there is a
+      pending higher-or-equal priority job at time [t]. Thus, the
+      assumption that the schedule respects priority policy at
+      preemption points implies that the scheduled job must have a
+      higher-or-equal priority. *)
+  Lemma scheduled_at_preemption_time_implies_higher_or_equal_priority_lt:
+    t < t2.-1 ->
+    forall jhp,
+      scheduled_at sched jhp t ->
+      hep_job jhp j.
+  Proof.
+    intros LTt2m1 jlp Sched_jlp; apply contraT; move => /negP NOTHP; exfalso.
+    move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
+    apply NOTQUIET with (t := t.+1).
+    { apply/andP; split.
+      - by apply leq_ltn_trans with t1.
+      - rewrite -subn1 ltn_subRL addnC in LTt2m1.
+        by rewrite -[t.+1]addn1.
+    }
+    intros j_hp ARR HP BEF.
+    apply contraT => NCOMP'; exfalso.
+    have PEND : pending sched j_hp t.
+    { apply/andP; split.
+      - by rewrite /has_arrived.
+      - by move: NCOMP'; apply contra, completion_monotonic.
+    }
+    apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
+    have HEP : hep_job j' j by apply (H_priority_is_transitive j_hp).
+    clear HEP' NCOMP' BEF HP ARR j_hp.
+    have BACK: backlogged sched j' t.
+    { apply/andP; split=> [//|].
+      apply/negP; intro SCHED'.
+      move: (H_uni jlp j' sched t Sched_jlp SCHED') => EQ.
+      by subst; apply: NOTHP.
+    }
+    apply NOTHP, (H_priority_is_transitive j'); last by eapply HEP.
+    by eapply H_respects_policy; eauto .
+  Qed.
+
+  (** In the case when [t = t2 - 1], we cannot use the same proof
+      since [t+1 = t2], but [t2] is a quiet time. So we do a similar
+      case analysis on the fact that [t1 = t ∨ t1 < t]. *)
+  Lemma scheduled_at_preemption_time_implies_higher_or_equal_priority_eq:
+    t = t2.-1 ->
+    forall jhp,
+      scheduled_at sched jhp t ->
+      hep_job jhp j.
+  Proof.
+    intros EQUALt2m1 jlp Sched_jlp; apply contraT; move => /negP NOTHP; exfalso.
+    move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
+    rewrite leq_eqVlt in GEt; first move: GEt => /orP [/eqP EQUALt1 | LARGERt1].
+    { subst t t1; clear LEt SL.
+      have ARR : job_arrival j = t2.-1.
+      { apply/eqP; rewrite eq_sym eqn_leq.
+        destruct t2 => [//|].
+        rewrite ltnS -pred_Sn in INBI.
+        by rewrite -pred_Sn.
+      }
+      have PEND: pending sched j t2.-1
+        by rewrite -ARR; apply job_pending_at_arrival.
+      apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].
+      eapply NOTHP, H_priority_is_transitive; last by apply HEPhp.
+      apply (H_respects_policy _ _ t2.-1); auto.
+      apply/andP; split=> [//|].
+      apply/negP; intros SCHED.
+      move: (H_uni _ _ sched _ SCHED Sched_jlp) => EQ.
+      by subst; apply: NOTHP.
+    }
+    { feed (NOTQUIET t); first by apply/andP; split.
+      apply NOTQUIET; intros j_hp' IN HP ARR.
+      apply contraT => NOTCOMP'; exfalso.
+      have PEND : pending sched j_hp' t.
+      { apply/andP; split.
+        - by rewrite /has_arrived ltnW.
+        - by move: NOTCOMP'; apply contra, completion_monotonic.
+      }
+      apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
+      have HEP : hep_job j' j by apply (H_priority_is_transitive j_hp').
+      clear ARR HP IN HEP' NOTCOMP' j_hp'.
+      have BACK: backlogged sched j' t.
+      { apply/andP; split=> [//|].
+        apply/negP; intro SCHED'.
+        move: (H_uni jlp j' sched t Sched_jlp SCHED') => EQ.
+        by subst; apply: NOTHP.
+      }
+      apply NOTHP, (H_priority_is_transitive j'); last by eapply HEP.
+      by eapply H_respects_policy; eauto .
+    }
+  Qed.
+
+  (** By combining the above facts we conclude that a job that is
+      scheduled at time [t] has higher-or-equal priority. *)
+  Corollary scheduled_at_preemption_time_implies_higher_or_equal_priority:
+    forall jhp,
+      scheduled_at sched jhp t ->
+      hep_job jhp j.
+  Proof.
+    move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
+    have: t <= t2.-1 by rewrite -subn1 leq_subRL_impl // addn1.
+    rewrite leq_eqVlt => /orP [/eqP EQUALt2m1 | LTt2m1].
+    - by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_eq.
+    - by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_lt.
+  Qed.
+
+  (** Since a job that is scheduled at time [t] has higher-or-equal
+      priority, by properties of a busy interval it cannot arrive
+      before time instant [t1]. *)
+  Lemma scheduled_at_preemption_time_implies_arrived_between_within_busy_interval:
+    forall jhp,
+      scheduled_at sched jhp t ->
+      arrived_between jhp t1 t2.
+  Proof.
+    intros jhp Sched_jhp.
+    rename H_work_conserving into WORK.
+    move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET INBI]]].
+    move: (H_t_in_busy_interval) => /andP [GEt LEt].
+    have HP := scheduled_at_preemption_time_implies_higher_or_equal_priority _ Sched_jhp.
+    move: (Sched_jhp) => PENDING.
+    eapply scheduled_implies_pending in PENDING => //.
+    apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _].
+    apply contraT; rewrite -ltnNge; intro LT; exfalso.
+    feed (QUIET jhp) => //.
+    specialize (QUIET HP LT).
+    have COMP: completed_by sched jhp t by apply: completion_monotonic QUIET.
+    apply completed_implies_not_scheduled in COMP => //.
+    by move: COMP => /negP COMP; apply COMP.
+  Qed.
+
+  (** From the above lemmas we prove that there is a job [jhp] that is
+      (1) scheduled at time [t], (2) has higher-or-equal priority, and
+      (3) arrived between [t1] and [t2].  *)
+  Corollary not_quiet_implies_exists_scheduled_hp_job_at_preemption_point:
+    exists j_hp,
+      arrived_between j_hp t1 t2
+      /\ hep_job j_hp j
+      /\ scheduled_at sched j_hp t.
+  Proof.
+    move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET INBI]]].
+    move: (H_t_in_busy_interval) => /andP [GEt LEt].
+    have [IDLE|[j' SCHED]] := scheduled_at_cases _ H_valid_arrivals sched ltac:(by []) ltac:(by []) t.
+    - by exfalso; apply instant_t_is_not_idle.
+    - exists j'; repeat split => //.
+      * exact: scheduled_at_preemption_time_implies_arrived_between_within_busy_interval.
+      * exact: scheduled_at_preemption_time_implies_higher_or_equal_priority.
+  Qed.
+
+End ProcessorBusyWithHEPJobAtPreemptionPoints.
+
+(** * Processor Executes HEP Jobs after Preemption Point *)
+(** In this section, we prove that at any time instant after any
+    preemption point (inside the busy interval), the processor is
+    always busy scheduling a job with higher or equal priority. *)
+Section ProcessorBusyWithHEPJobAfterPreemptionPoints.
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
+
+  (** ... and any uniprocessor schedule of this arrival sequence. *)
+  Context {PState : ProcessorState Job}.
+  Hypothesis H_uni : uniprocessor_model PState.
+  Variable sched : schedule PState.
+
+  (** Consider a JLFP policy that indicates a higher-or-equal priority relation,
+      and assume that the relation is reflexive and transitive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
+  Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
+
+  (** Consider a valid preemption model with known maximum non-preemptive
+      segment lengths. *)
+  Context `{TaskMaxNonpreemptiveSegment Task} `{JobPreemptable Job}.
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** Further, allow for any work-bearing notion of job readiness. *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** We assume that the schedule is valid. *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** Next, we assume that the schedule is work-conserving ... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** ... and the schedule respects the scheduling policy at every preemption point. *)
+  Hypothesis H_respects_policy :
+    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
+
+  (** Consider any job [j] with positive job cost. *)
+  Variable j : Job.
+  Hypothesis H_j_arrives : arrives_in arr_seq j.
+  Hypothesis H_job_cost_positive : job_cost_positive j.
+
+  (** Consider any busy interval prefix <<[t1, t2)>> of job [j]. *)
+  Variable t1 t2 : instant.
+  Hypothesis H_busy_interval_prefix :
+    busy_interval_prefix arr_seq sched j t1 t2.
+
+  (** First, recall from the above section that the processor at any
+      preemption time is always busy scheduling a job with higher or equal
+      priority. *)
+
+  (** We show that, at any time instant after a preemption point, the
+      processor is always busy with a job with higher or equal
+      priority. *)
+  Lemma not_quiet_implies_exists_scheduled_hp_job_after_preemption_point:
+    forall tp t,
+      preemption_time arr_seq sched tp ->
+      t1 <= tp < t2 ->
+      tp <= t < t2 ->
+      exists j_hp,
+        arrived_between j_hp t1 t.+1 /\
+          hep_job j_hp j /\
+          scheduled_at sched j_hp t.
+  Proof.
+    move => tp t PRPOINT /andP [GEtp LTtp] /andP [LEtp LTt].
+    have [Idle|[jhp Sched_jhp]] :=
+      scheduled_at_cases _ H_valid_arrivals sched ltac:(by []) ltac:(by []) t.
+    { eapply instant_t_is_not_idle in Idle => //.
+      by apply/andP; split; first apply leq_trans with tp. }
+    exists jhp.
+    have HP: hep_job jhp j.
+    { have PP := scheduling_of_any_segment_starts_with_preemption_time _
+                   arr_seq  H_valid_arrivals
+                   sched H_sched_valid H_valid_preemption_model jhp t Sched_jhp.
+      feed PP => //.
+      move: PP => [prt [/andP [_ LE] [PR SCH]]].
+      case E:(t1 <= prt).
+      - move: E => /eqP /eqP E; rewrite subn_eq0 in E.
+        edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point as [jlp [_ [HEP SCHEDjhp]]] => //.
+        { by apply /andP; split; last by apply leq_ltn_trans with t. }
+        enough (EQ : jhp = jlp); first by subst.
+        apply: (H_uni _ _ _ prt); eauto;
+          by apply SCH; apply/andP; split.
+      - move: E => /eqP /neqP E; rewrite -lt0n subn_gt0 in E.
+        apply negbNE; apply/negP; intros LP; rename jhp into jlp.
+        edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point
+          as [jhp [_ [HEP SCHEDjhp]]]; try apply PRPOINT; move=> //.
+        * by apply/andP; split.
+        * move: LP => /negP LP; apply: LP.
+          enough (EQ : jhp = jlp); first by subst.
+          apply: (H_uni jhp _ _ tp); eauto.
+          by apply SCH; apply/andP; split; first apply leq_trans with t1; auto. }
+    repeat split=> //.
+    move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET EXj]]]; move: (Sched_jhp) => PENDING.
+    eapply scheduled_implies_pending in PENDING => //.
+    apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _].
+    apply contraT; rewrite -ltnNge; intro LT; exfalso.
+    feed (QUIET jhp) => //.
+    specialize (QUIET HP LT).
+    move: Sched_jhp; apply/negP/completed_implies_not_scheduled => //.
+    apply: completion_monotonic QUIET.
+    exact: leq_trans LEtp.
+  Qed.
+
+  (** Now, suppose there exists some constant [K] that bounds the
+      distance to a preemption time from the beginning of the busy
+      interval. *)
+  Variable K : duration.
+  Hypothesis H_preemption_time_exists :
+    exists pr_t, preemption_time arr_seq sched pr_t /\ t1 <= pr_t <= t1 + K.
+
+  (** Then we prove that the processor is always busy with a job
+      with higher-or-equal priority after time instant [t1 + K]. *)
+  Lemma not_quiet_implies_exists_scheduled_hp_job:
+    forall t,
+      t1 + K <= t < t2 ->
+      exists j_hp,
+        arrived_between j_hp t1 t.+1 /\
+          hep_job j_hp j /\
+          scheduled_at sched j_hp t.
+  Proof.
+    move => t /andP [GE LT].
+    move: H_preemption_time_exists => [prt [PR /andP [GEprt LEprt]]].
+    apply not_quiet_implies_exists_scheduled_hp_job_after_preemption_point with (tp := prt); eauto 2.
+    - apply/andP; split=> [//|].
+      apply leq_ltn_trans with (t1 + K) => [//|].
+      by apply leq_ltn_trans with t.
+    - apply/andP; split=> [|//].
+      by apply leq_trans with (t1 + K).
+  Qed.
+
+End ProcessorBusyWithHEPJobAfterPreemptionPoints.

analysis/facts/busy_interval/pi.v

+Require Export prosa.model.task.preemption.parameters.
+Require Export prosa.analysis.facts.model.preemption.
+Require Export prosa.analysis.facts.busy_interval.hep_at_pt.
+
+(** * Priority Inversion in a Busy Interval *)
+(** In this module, we reason about priority inversion that occurs during a busy
+    interval due to non-preemptive sections. *)
+Section PriorityInversionIsBounded.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any valid arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
+
+  (** ... and any uniprocessor schedule of this arrival sequence. *)
+  Context {PState : ProcessorState Job}.
+  Hypothesis H_uni : uniprocessor_model PState.
+  Variable sched : schedule PState.
+
+  (** Consider a JLFP policy that indicates a higher-or-equal priority relation,
+      and assume that the relation is reflexive and transitive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
+  Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
+
+  (** Consider a valid preemption model with known maximum non-preemptive
+      segment lengths. *)
+  Context `{TaskMaxNonpreemptiveSegment Task} `{JobPreemptable Job}.
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** Further, allow for any work-bearing notion of job readiness. *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** We assume that the schedule is valid ... *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** ... and that the schedule respects the scheduling policy at every
+      preemption point. *)
+  Hypothesis H_respects_policy :
+    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
+
+  (** Consider any job [j] of [tsk] with positive job cost. *)
+  Variable j : Job.
+  Hypothesis H_j_arrives : arrives_in arr_seq j.
+  Hypothesis H_job_cost_positive : job_cost_positive j.
+
+  (** Consider any busy interval prefix <<[t1, t2)>> of job [j]. *)
+  Variable t1 t2 : instant.
+  Hypothesis H_busy_interval_prefix :
+    busy_interval_prefix arr_seq sched j t1 t2.
+
+  (** ** Lower Priority In Busy Intervals *)
+  (** First, we state some basic properties about a lower priority job executing
+      in the busy interval of the job under consideration. From the definition
+      of the busy interval it follows that a lower priority job can only be
+      executing inside the busy interval as a result of priority inversion. *)
+  Section LowerPriorityJobScheduled.
+
+    (** Consider a lower-priority job. *)
+    Variable jlp : Job.
+    Hypothesis H_jlp_lp : ~~hep_job jlp j.
+
+    (** Consider an instant [t] within the busy window of the job such that
+        [jlp] is scheduled at [t]. *)
+    Variable t : instant.
+    Hypothesis H_t_in_busy : t1 <= t < t2.
+    Hypothesis H_jlp_scheduled_at_t : scheduled_at sched jlp t.
+
+    (** First, we prove that no time from [t1] up to the instant [t] can
+        be a preemption point. *)
+    Lemma lower_priority_job_scheduled_implies_no_preemption_time :
+      forall t',
+        t1 <= t' <= t ->
+        ~~ preemption_time arr_seq sched t'.
+    Proof.
+      move => t' /andP[LE1 GT1].
+      apply /negP => PT.
+      move: H_jlp_lp => /negP LP; apply: LP.
+      have [ptst [IN1 [PTT STT]]] : exists ptst : nat,
+          t' <= ptst <= t /\ preemption_time arr_seq sched ptst /\ scheduled_at sched jlp ptst.
+      { by apply: scheduling_of_any_segment_starts_with_preemption_time_continuously_sched => //=. }
+      apply: (scheduled_at_preemption_time_implies_higher_or_equal_priority arr_seq _ sched _ _ _ _ j _ _ t1 t2 _ ptst)  => //.
+      by lia.
+    Qed.
+
+    (** Then it follows that the job must have been continuously scheduled from
+        [t1] up to [t]. *)
+    Lemma lower_priority_job_continuously_scheduled:
+      forall t',
+        t1 <= t' <= t ->
+        scheduled_at sched jlp t'.
+    Proof.
+      move => t' IN.
+      move : IN => /andP [IN1' IN2'].
+      apply: neg_pt_scheduled_continuously_after => //.
+      move => ??.
+      apply lower_priority_job_scheduled_implies_no_preemption_time.
+      by lia.
+    Qed.
+
+    (** Any lower-priority jobs that are scheduled inside the
+        busy-interval prefix <<[t1,t2)>> must arrive before that interval. *)
+    Lemma low_priority_job_arrives_before_busy_interval_prefix:
+      job_arrival jlp < t1.
+    Proof.
+      have SCHED1 : scheduled_at sched jlp t1.
+      { apply lower_priority_job_continuously_scheduled => //. lia. }
+      have ARR1: job_arrival jlp <= t1 by apply: (has_arrived_scheduled sched jlp _ t1 SCHED1).
+      rewrite /has_arrived leq_eqVlt in ARR1.
+      move : ARR1 => /orP[/eqP EQ| ?]; last by done.
+      exfalso.
+      have PP := scheduling_of_any_segment_starts_with_preemption_time _
+                   arr_seq H_valid_arrivals
+                   sched H_sched_valid
+                   H_valid_preemption_model jlp t H_jlp_scheduled_at_t.
+      feed PP => //.
+      move: PP => [pt [/andP [NEQ1 NEQ2] [PT FA]]].
+      contradict PT.
+      apply /negP.
+      by apply (lower_priority_job_scheduled_implies_no_preemption_time ) => //=; lia.
+    Qed.
+
+    (** Finally, we show that lower-priority jobs that are scheduled
+        inside the busy-interval prefix <<[t1,t2)>> must also be scheduled
+        before the interval. *)
+    Lemma low_priority_job_scheduled_before_busy_interval_prefix:
+      exists t', t' < t1 /\ scheduled_at sched jlp t'.
+    Proof.
+      move: H_t_in_busy => /andP [GE LT].
+      have ARR := low_priority_job_arrives_before_busy_interval_prefix .
+      exists t1.-1; split.
+      { by rewrite prednK; last apply leq_ltn_trans with (job_arrival jlp). }
+      eapply neg_pt_scheduled_at => //.
+      - rewrite prednK; last by apply leq_ltn_trans with (job_arrival jlp).
+        apply lower_priority_job_continuously_scheduled => //. lia.
+      - rewrite prednK; last by apply leq_ltn_trans with (job_arrival jlp).
+        apply lower_priority_job_scheduled_implies_no_preemption_time.
+        by lia.
+    Qed.
+
+  End LowerPriorityJobScheduled.
+
+
+  (** In this section, we prove that priority inversion only
+      occurs at the start of the busy window and occurs due to only
+      one job. *)
+  Section SingleJob.
+
+    (** Suppose job [j] incurs priority inversion at a time [t_pi] in its busy window. *)
+    Variable t_pi : instant.
+    Hypothesis H_from_t1_before_t2 : t1 <= t_pi < t2.
+    Hypothesis H_PI_occurs : priority_inversion arr_seq sched j t_pi.
+
+    (** First, we show that there is no preemption time in the interval <<[t1,t_pi]>>. *)
+    Lemma no_preemption_time_before_pi :
+      forall t,
+        t1 <= t <= t_pi ->
+        ~~ preemption_time arr_seq sched t.
+    Proof.
+      move => ppt intl.
+      move : H_PI_occurs => /uni_priority_inversion_P PI.
+      feed_n 5 PI => //=.
+      move : PI => [jlp SCHED NHEP].
+      by apply (lower_priority_job_scheduled_implies_no_preemption_time jlp NHEP t_pi).
+    Qed.
+
+    (** Next, we show that the same job will be scheduled from the start of the 
+        busy interval to the priority inversion time [t_pi]. *)
+    Lemma pi_job_remains_scheduled :
+      forall jlp,
+        scheduled_at sched jlp t_pi ->
+        forall t,
+          t1 <= t <= t_pi -> scheduled_at sched jlp t.
+    Proof.
+      move : H_PI_occurs => /uni_priority_inversion_P PI.
+      feed_n 5 PI => //=.
+      move : PI => [jlp SCHED NHEP].
+      move => jlp1 SCHED3 t IN.
+      apply: lower_priority_job_continuously_scheduled => //.
+      by have -> : jlp1 = jlp.
+    Qed.
+
+    (** Thus, priority inversion takes place from the start of the busy interval
+        to the instant [t_pi], i.e., priority inversion takes place
+        continuously. *)
+    Lemma pi_continuous :
+      forall t,
+        t1 <= t <= t_pi ->
+        priority_inversion arr_seq sched j t.
+    Proof.
+      move: (H_PI_occurs) => /andP[j_nsched_pi /hasP[jlp jlp_sched_pi nHEPj]] t INTL.
+      apply /uni_priority_inversion_P => // ; exists jlp => //.
+      apply: pi_job_remains_scheduled => //.
+      by rewrite -(scheduled_jobs_at_iff arr_seq).
+    Qed.
+
+  End SingleJob.
+
+  (** As a simple corollary to the lemmas proved in the previous
+      section, we show that for any two jobs [j1] and [j2] that cause
+      priority inversion to job [j], it is the case that [j1 = j2]. *)
+  Section SingleJobEq.
+
+    (** Consider a time instant [ts1] in <<[t1, t2)>> ... *)
+    Variable ts1 : instant.
+    Hypothesis H_ts1_in_busy_prefix : t1 <= ts1 < t2.
+
+    (** ... and a lower-priority (w.r.t. job [j]) job [j1] that is
+        scheduled at time [ts1]. *)
+    Variable j1 : Job.
+    Hypothesis H_j1_sched : scheduled_at sched j1 ts1.
+    Hypothesis H_j1_lower_prio : ~~ hep_job j1 j.
+
+    (** Similarly, consider a time instant [ts2] in <<[t1, t2)>> ... *)
+    Variable ts2 : instant.
+    Hypothesis H_ts2_in_busy_prefix : t1 <= ts2 < t2.
+
+    (** ... and a lower-priority job [j2] that is scheduled at time [ts2]. *)
+    Variable j2 : Job.
+    Hypothesis H_j2_sched : scheduled_at sched j2 ts2.
+    Hypothesis H_j2_lower_prio : ~~ hep_job j2 j.
+
+    (** Then, [j1] is equal to [j2]. *)
+    Corollary only_one_pi_job :
+      j1 = j2.
+    Proof.
+      have [NEQ|NEQ] := leqP ts1 ts2.
+      { apply: H_uni; first by apply H_j1_sched.
+        apply: pi_job_remains_scheduled; try apply H_j2_sched; try lia.
+        by erewrite priority_inversion_hep_job.
+      }
+      { apply: H_uni; last by apply H_j2_sched.
+        apply: pi_job_remains_scheduled; try apply H_j1_sched; try lia.
+        by erewrite priority_inversion_hep_job; try apply H_j1_sched.
+      }
+    Qed.
+
+  End SingleJobEq.
+
+  (** From the above lemmas, it follows that either job [j] incurs no priority
+      inversion at all or certainly at time [t1], i.e., the beginning of its
+      busy interval. *)
+  Lemma busy_interval_pi_cases :
+    cumulative_priority_inversion arr_seq sched j t1 t2 = 0
+    \/ priority_inversion arr_seq sched j t1.
+  Proof.
+    case: (posnP (cumulative_priority_inversion arr_seq sched j t1 t2)); first by left.
+    rewrite sum_nat_gt0 // => /hasP[pi].
+    rewrite mem_filter /= mem_index_iota lt0b => INTL PI_pi.
+    by right; apply: pi_continuous =>//; lia.
+  Qed.
+
+  (** Next, we use the above facts to establish bounds on the maximum priority
+      inversion that can be incurred in a busy interval. *)
+
+  (** * Priority Inversion due to Non-Preemptive Sections *)
+
+  (** First, we introduce the notion of the maximum length of a
+      nonpreemptive segment among all lower priority jobs (w.r.t. a
+      given job [j]) arrived so far. *)
+  Definition max_lp_nonpreemptive_segment (j : Job) (t : instant) :=
+    \max_(j_lp <- arrivals_before arr_seq t | (~~ hep_job j_lp j) && (job_cost j_lp > 0))
+      (job_max_nonpreemptive_segment j_lp - ε).
+
+  (** Note that any bound on the [max_lp_nonpreemptive_segment]
+      function is also be a bound on the maximum priority inversion
+      (assuming there are no other mechanisms that could cause
+      priority inversion). This bound may be different for different
+      scheduler and/or task models. Thus, we don't define such a bound
+      in this module. *)
+
+  Section TaskMaxNPS.
+
+    (** First, assuming proper non-preemptive sections, ... *)
+    Hypothesis H_valid_nps :
+      valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+    (** ... we observe that the maximum non-preemptive segment length
+        of any task that releases a job with lower priority (w.r.t. a
+        given job [j]) and non-zero execution cost upper-bounds the
+        maximum possible non-preemptive segment length of any
+        lower-priority job. *)
+    Lemma max_np_job_segment_bounded_by_max_np_task_segment :
+      max_lp_nonpreemptive_segment j t1
+      <= \max_(j_lp <- arrivals_between arr_seq 0 t1 | (~~ hep_job j_lp j)
+                                                     && (job_cost j_lp > 0))
+          (task_max_nonpreemptive_segment (job_task j_lp) - ε).
+    Proof.
+      rewrite /max_lp_nonpreemptive_segment.
+      apply: leq_big_max => j' JINB NOTHEP.
+      rewrite leq_sub2r //.
+      apply in_arrivals_implies_arrived in JINB.
+      by apply H_valid_nps.
+    Qed.
+
+  End TaskMaxNPS.
+
+  (** Next, we prove that the function [max_lp_nonpreemptive_segment]
+      indeed upper-bounds the priority inversion length. *)
+  Section PreemptionTimeExists.
+
+    (** In this section, we require the jobs to have valid bounded
+        non-preemptive segments. *)
+    Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+      valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+    (** First, we prove that, if a job with higher-or-equal priority is scheduled at
+        a quiet time [t+1], then this is the first time when this job is scheduled. *)
+    Lemma hp_job_not_scheduled_before_quiet_time :
+      forall jhp t,
+        quiet_time arr_seq sched j t.+1 ->
+        scheduled_at sched jhp t.+1 ->
+        hep_job jhp j ->
+        ~~ scheduled_at sched jhp t.
+    Proof.
+      intros jhp t QT SCHED1 HP.
+      apply/negP; intros SCHED2.
+      specialize (QT jhp).
+      feed_n 3 QT => //.
+      - have MATE: jobs_must_arrive_to_execute sched by [].
+        by have HA: has_arrived jhp t by exact: MATE.
+      - apply completed_implies_not_scheduled in QT => //.
+        by move: QT => /negP NSCHED; apply: NSCHED.
+    Qed.
+
+    (** Thus, there must be a preemption time in the interval [t1, t1
+        + max_lp_nonpreemptive_segment j t1]. That is, if a job with
+        higher-or-equal priority is scheduled at time instant [t1],
+        then [t1] is a preemption time. Otherwise, if a job with lower
+        priority is scheduled at time [t1], then this job also should
+        be scheduled before the beginning of the busy interval. So,
+        the next preemption time will be no more than
+        [max_lp_nonpreemptive_segment j t1] time units later. *)
+
+    (** We proceed by doing a case analysis. *)
+    Section CaseAnalysis.
+
+      (** (1) Case when the schedule is idle at time [t1]. *)
+      Section Case1.
+
+        (** Assume that the schedule is idle at time [t1]. *)
+        Hypothesis H_is_idle : is_idle arr_seq sched t1.
+
+        (** Then time instant [t1] is a preemption time. *)
+        Lemma preemption_time_exists_case1:
+          exists pr_t,
+            preemption_time arr_seq sched pr_t 
+            /\ t1 <= pr_t <= t1 + max_lp_nonpreemptive_segment j t1.
+        Proof.
+          set (service := service sched).
+          move: (H_valid_model_with_bounded_nonpreemptive_segments) => CORR.
+          move: (H_busy_interval_prefix) => [NEM [QT1 [NQT HPJ]]].
+          exists t1; split.
+          - exact: idle_time_is_pt.
+          - by apply/andP; split; last rewrite leq_addr.
+        Qed.
+
+      End Case1.
+
+      (** (2) Case when a job with higher-or-equal priority is scheduled at time [t1]. *)
+      Section Case2.
+
+        (** Assume that a job [jhp] with higher-or-equal priority is scheduled at time [t1]. *)
+        Variable jhp : Job.
+        Hypothesis H_jhp_is_scheduled : scheduled_at sched jhp t1.
+        Hypothesis H_jhp_hep_priority : hep_job jhp j.
+
+        (** Then time instant [t1] is a preemption time. *)
+        Lemma preemption_time_exists_case2:
+          exists pr_t,
+            preemption_time arr_seq sched pr_t /\
+            t1 <= pr_t <= t1 + max_lp_nonpreemptive_segment j t1.
+        Proof.
+          set (service := service sched).
+          move :  (H_valid_model_with_bounded_nonpreemptive_segments) =>  [VALID BOUNDED].
+          move: (H_valid_model_with_bounded_nonpreemptive_segments) => CORR.
+          move: (H_busy_interval_prefix) => [NEM [QT1 [NQT HPJ]]].
+          exists t1; split; last by apply/andP; split; [|rewrite leq_addr].
+          destruct t1.
+          - exact: zero_is_pt.
+          - apply: first_moment_is_pt H_jhp_is_scheduled => //.
+            exact: hp_job_not_scheduled_before_quiet_time.
+        Qed.
+
+      End Case2.
+
+      (** The following argument requires a unit-service assumption. *)
+      Hypothesis H_unit : unit_service_proc_model PState.
+
+      (** (3) Case when a job with lower priority is scheduled at time [t1]. *)
+      Section Case3.
+
+        (** Assume that a job [jhp] with lower priority is scheduled at time [t1]. *)
+        Variable jlp : Job.
+        Hypothesis H_jlp_is_scheduled : scheduled_at sched jlp t1.
+        Hypothesis H_jlp_low_priority : ~~ hep_job jlp j.
+
+        (** To prove the lemma in this case we need a few auxiliary
+            facts about the first preemption point of job [jlp]. *)
+        Section FirstPreemptionPointOfjlp.
+
+          (** Let's denote the progress of job [jlp] at time [t1] as [progr_t1]. *)
+          Let progr_t1 := service sched jlp t1.
+
+          (** Consider the first preemption point of job [jlp] after [progr_t1]. *)
+          Variable fpt : instant.
+          Hypothesis H_fpt_is_preemption_point : job_preemptable jlp (progr_t1 + fpt).
+          Hypothesis H_fpt_is_first_preemption_point :
+            forall ρ,
+              progr_t1 <= ρ <= progr_t1 + (job_max_nonpreemptive_segment jlp - ε) ->
+              job_preemptable jlp ρ ->
+              service sched jlp t1 + fpt <= ρ.
+
+          (** For correctness, we also assume that [fpt] does not
+              exceed the length of the maximum non-preemptive
+              segment. *)
+          Hypothesis H_progr_le_max_nonp_segment :
+            fpt <= job_max_nonpreemptive_segment jlp - ε.
+
+          (** First we show that [fpt] is indeed the first preemption point after [progr_t1]. *)
+          Lemma no_intermediate_preemption_point:
+            forall ρ,
+              progr_t1 <= ρ < progr_t1 + fpt ->
+              ~~ job_preemptable jlp ρ.
+          Proof.
+            move => prog /andP [GE LT].
+            apply/negP; intros PPJ.
+            move: H_fpt_is_first_preemption_point => K; specialize (K prog).
+            feed_n 2 K => [|//|]; first (apply/andP; split=> //).
+            { apply leq_trans with (service sched jlp t1 + fpt).
+              + exact: ltnW.
+              + by rewrite leq_add2l; apply H_progr_le_max_nonp_segment.
+            }
+            by move: K; rewrite leqNgt; move => /negP NLT; apply: NLT.
+          Qed.
+
+          (** Thanks to the fact that the scheduler respects the notion of preemption points
+              we show that [jlp] is continuously scheduled in time interval <<[t1, t1 + fpt)>>. *)
+          Lemma continuously_scheduled_between_preemption_points:
+            forall t',
+              t1 <= t' < t1 + fpt ->
+              scheduled_at sched jlp t'.
+          Proof.
+            move: (H_valid_model_with_bounded_nonpreemptive_segments) => CORR.
+            have ARRs : arrives_in arr_seq jlp by [].
+            move => t' /andP [GE LT].
+            have Fact: exists Δ, t' = t1 + Δ.
+            { by exists (t' - t1); apply/eqP; rewrite eq_sym; apply/eqP; rewrite subnKC. }
+            move: Fact => [Δ EQ]; subst t'.
+            have NPPJ := @no_intermediate_preemption_point (@service _ _ sched jlp (t1 + Δ)).
+            apply proj1 in CORR; specialize (CORR jlp ARRs).
+            move: CORR => [_ [_ [T _] ]].
+            apply T; apply: NPPJ; apply/andP; split.
+            { by apply service_monotonic; rewrite leq_addr. }
+            rewrite /service  -(service_during_cat _ _ _ t1).
+            { rewrite ltn_add2l; rewrite ltn_add2l in LT.
+              apply leq_ltn_trans with Δ => [|//].
+              rewrite -{2}(sum_of_ones t1 Δ).
+              by rewrite leq_sum. }
+            { by apply/andP; split; [|rewrite leq_addr]. }
+          Qed.
+
+          (** Thus, assuming an ideal-progress processor model, job [jlp]
+              reaches its preemption point at time instant [t1 + fpt], which
+              implies that time instant [t1 + fpt] is a preemption time. *)
+          Lemma first_preemption_time :
+            ideal_progress_proc_model PState ->
+            preemption_time arr_seq sched (t1 + fpt).
+          Proof.
+            move=> H_progress.
+            have [IDLE|[j' SCHED']] :=
+              scheduled_at_cases _ H_valid_arrivals sched ltac:(by []) ltac:(by []) (t1 + fpt);
+              first exact: idle_time_is_pt.
+            have [EQ|NEQ] := (eqVneq jlp j').
+            { move: (SCHED'); rewrite -(scheduled_job_at_scheduled_at arr_seq) // -EQ /preemption_time => /eqP ->.
+              rewrite  /service -(service_during_cat _ _ _ t1); last first.
+              { by apply/andP; split; last rewrite leq_addr. }
+              have ->: service_during sched jlp t1 (t1 + fpt) = fpt => //.
+              { rewrite -{2}(sum_of_ones t1 fpt) /service_during.
+                apply/eqP; rewrite eqn_leq //; apply/andP; split.
+                + by rewrite leq_sum.
+                + rewrite big_nat_cond [in X in _ <= X]big_nat_cond.
+                  rewrite leq_sum //.
+                  move => x /andP [HYP _].
+                  exact/H_progress/continuously_scheduled_between_preemption_points. } }
+            { case: (posnP fpt) => [ZERO|POS].
+              { subst fpt; rewrite addn0 in SCHED'.
+                exfalso; move: NEQ => /negP; apply; apply/eqP.
+                exact: H_uni. }
+              { have [sm EQ2]: exists sm, sm.+1 = fpt by exists fpt.-1; rewrite prednK.
+                move: SCHED'; rewrite -EQ2 addnS => SCHED'.
+                apply:  first_moment_is_pt (SCHED') => //.
+                apply: scheduled_job_at_neq => //.
+                apply: (continuously_scheduled_between_preemption_points (t1 + sm)).
+                by apply/andP; split; [rewrite leq_addr | rewrite -EQ2 addnS]. } }
+          Qed.
+
+          (** And since [fpt <= max_lp_nonpreemptive_segment j t1],
+              [t1 <= t1 + fpt <= t1 + max_lp_nonpreemptive_segment j t1]. *)
+          Lemma preemption_time_le_max_len_of_np_segment :
+            t1 <= t1 + fpt <= t1 + max_lp_nonpreemptive_segment j t1.
+          Proof.
+            have ARRs : arrives_in arr_seq jlp by [].
+            apply/andP; split; first by rewrite leq_addr.
+            rewrite leq_add2l.
+            unfold max_lp_nonpreemptive_segment.
+            rewrite (big_rem jlp) //=.
+            { rewrite H_jlp_low_priority //=.
+              have NZ: service sched jlp t1 < job_cost jlp by exact: service_lt_cost.
+              rewrite ifT; last lia.
+              apply leq_trans with (job_max_nonpreemptive_segment jlp - ε).
+              - by apply H_progr_le_max_nonp_segment.
+              - by rewrite leq_maxl.
+            }
+            apply: arrived_between_implies_in_arrivals => [//|//|].
+            apply/andP; split=> [//|].
+            eapply low_priority_job_arrives_before_busy_interval_prefix with t1; eauto 2.
+            by move: (H_busy_interval_prefix) => [NEM [QT1 [NQT HPJ]]]; apply/andP.
+          Qed.
+
+        End FirstPreemptionPointOfjlp.
+
+        (** For the next step, we assume an ideal-progress processor. *)
+        Hypothesis H_progress : ideal_progress_proc_model PState.
+
+        (** Next, we combine the above facts to conclude the lemma. *)
+        Lemma preemption_time_exists_case3:
+          exists pr_t,
+            preemption_time arr_seq sched pr_t /\
+            t1 <= pr_t <= t1 + max_lp_nonpreemptive_segment j t1.
+        Proof.
+          set (service := service sched).
+          have EX: exists pt,
+              ((service jlp t1) <= pt <= (service jlp t1) + (job_max_nonpreemptive_segment jlp - 1)) && job_preemptable jlp pt.
+          { have ARRs: arrives_in arr_seq jlp by [].
+            move: (proj2 (H_valid_model_with_bounded_nonpreemptive_segments) jlp ARRs) =>[_ EXPP].
+            destruct H_sched_valid as [A B].
+            specialize (EXPP (service jlp t1)).
+            feed EXPP.
+            { apply/andP; split=> [//|].
+              exact: service_at_most_cost.
+            }
+            move: EXPP => [pt [NEQ PP]].
+            by exists pt; apply/andP.
+          }
+          move: (ex_minnP EX) => [sm_pt /andP [NEQ PP] MIN]; clear EX.
+          have Fact: exists Δ, sm_pt = service jlp t1 + Δ.
+          { exists (sm_pt - service jlp t1).
+            apply/eqP; rewrite eq_sym; apply/eqP; rewrite subnKC //.
+            by move: NEQ => /andP [T _]. }
+          move: Fact => [Δ EQ]; subst sm_pt; rename Δ into sm_pt.
+          exists (t1 + sm_pt); split.
+          { apply first_preemption_time; rewrite /service.service//.
+            + by intros; apply MIN; apply/andP; split.
+            + by lia.
+          }
+          apply: preemption_time_le_max_len_of_np_segment => //.
+          by lia.
+        Qed.
+
+      End Case3.
+
+    End CaseAnalysis.
+
+    (** As Case 3 depends on unit-service and ideal-progress assumptions, we
+        require the same here. *)
+    Hypothesis H_unit : unit_service_proc_model PState.
+    Hypothesis H_progress : ideal_progress_proc_model PState.
+
+    (** By doing the case analysis, we show that indeed there is a
+        preemption time in the time interval [[t1, t1 +
+        max_lp_nonpreemptive_segment j t1]]. *)
+    Lemma preemption_time_exists :
+      exists pr_t,
+        preemption_time arr_seq sched pr_t /\
+        t1 <= pr_t <= t1 + max_lp_nonpreemptive_segment j t1.
+    Proof.
+      have [Idle|[s Sched_s]] :=
+        scheduled_at_cases _ H_valid_arrivals sched ltac:(by []) ltac:(by []) t1.
+      - by apply preemption_time_exists_case1.
+      - destruct (hep_job s j) eqn:PRIO.
+        + exact: preemption_time_exists_case2.
+        + apply: preemption_time_exists_case3 => //.
+          by rewrite -eqbF_neg; apply /eqP.
+    Qed.
+
+  End PreemptionTimeExists.
+
+  (** In this section we prove that if a preemption point [ppt] exists in a job's busy window,
+      it suffers no priority inversion after [ppt]. Equivalently the [cumulative_priority_inversion]
+      of the job in the busy window [t1,t2] is bounded by the [cumulative_priority_inversion]
+      of the job in the time window [t1,[ppt]). *)
+  Section NoPriorityInversionAfterPreemptionPoint.
+
+    (** Consider the preemption point [ppt]. *)
+    Variable ppt: instant.
+    Hypothesis H_preemption_point : preemption_time arr_seq sched ppt.
+    Hypothesis H_after_t1 : t1 <= ppt.
+
+    (** We first establish the aforementioned result by showing that [j] cannot
+        suffer priority inversion after the preemption time [ppt] ... *)
+    Lemma no_priority_inversion_after_preemption_point :
+      forall t,
+        ppt <= t < t2 ->
+        ~~ priority_inversion arr_seq sched j t.
+    Proof.
+      move=> t /andP [pptt tt2].
+      apply /negP => PI.
+      move: PI => /andP[j_nsched_pi /hasP[jlp jlp_sched_pi nHEPj]].
+      have [/eqP SCHED1 //|[j' /eqP SCHED2 //=]] :=
+        scheduled_jobs_at_uni_cases arr_seq ltac:(done) sched ltac:(done)
+                                                                     ltac:(done) ltac:(done) t; first by rewrite SCHED1 in jlp_sched_pi.
+      rewrite SCHED2 mem_seq1 in jlp_sched_pi.
+      move : jlp_sched_pi => /eqP HJLP.
+      replace j' with jlp in *; clear HJLP.
+      move : SCHED2 => /eqP SCHED2.
+      rewrite scheduled_jobs_at_scheduled_at in SCHED2 => //=.
+      have [ptst [IN1 [PTT STT]]] : exists ptst : nat,
+          ppt <= ptst <= t /\ preemption_time arr_seq sched ptst /\ scheduled_at sched jlp ptst.
+      { by apply: scheduling_of_any_segment_starts_with_preemption_time_continuously_sched. }
+       contradict nHEPj.
+       apply /negP /negPn.
+       apply: scheduled_at_preemption_time_implies_higher_or_equal_priority => //.
+       by lia.
+    Qed.
+
+    (** ... and then lift this fact to cumulative priority inversion. *)
+    Lemma priority_inversion_occurs_only_till_preemption_point :
+      cumulative_priority_inversion arr_seq sched j t1 t2 <=
+      cumulative_priority_inversion arr_seq sched j t1 ppt.
+    Proof.
+      have [LEQ|LT_t1t2] := leqP t1 t2;
+        last by rewrite /cumulative_priority_inversion big_geq //; exact: ltnW.
+      have [LEQ_t2ppt|LT] := leqP t2 ppt;
+        first by rewrite (cumulative_priority_inversion_cat _ _ _ t2 t1 ppt) //
+                 ; exact: leq_addr.
+      move: (H_busy_interval_prefix) => [_ [_ [_ /andP [T _]]]].
+      rewrite /cumulative_priority_inversion (@big_cat_nat _ _ _ ppt) //=.
+      rewrite -[X in _ <= X]addn0 leq_add2l leqn0.
+      rewrite big_nat_cond big1 //; move => t /andP[/andP[GEt LEt] _].
+      apply/eqP; rewrite eqb0.
+      by apply/no_priority_inversion_after_preemption_point/andP.
+    Qed.
+
+  End NoPriorityInversionAfterPreemptionPoint.
+
+End PriorityInversionIsBounded.

analysis/facts/busy_interval/pi_bound.v

+Require Export prosa.analysis.facts.busy_interval.pi.
+
+(** * Bounded Priority Inversion Due to Non-Preemptive Sections *)
+
+(** In the following, we relate the maximum cumulative priority inversion with a
+    given blocking bound, assuming that priority version is caused (only) by
+    non-preemptive segments. *)
+Section PriorityInversionIsBounded.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (** In addition, we assume that each task has a maximal non-preemptive
+    segment ... *)
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (**  ... and any type of preemptable jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobPreemptable Job}.
+
+  (** Consider any valid arrival sequence,... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Context {PState : ProcessorState Job}.
+  Variable sched : schedule PState.
+
+  (** Consider a JLFP policy that indicates a higher-or-equal priority relation,
+      and assume that the relation is reflexive and transitive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
+  Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
+
+  (** And assume that they define a valid preemption model with
+      bounded nonpreemptive segments. *)
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Further, allow for any work-bearing notion of job readiness. *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** We assume that the schedule is valid. *)
+  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
+
+  (** Next, we assume that the schedule is a work-conserving schedule... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** ...,it respects the scheduling policy at every preemption point,... *)
+  Hypothesis H_respects_policy :
+    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
+
+  (** ... and complies with the preemption model. *)
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** Now, we consider an arbitrary task set [ts]... *)
+  Variable ts : seq Task.
+
+  (** ... and assume that all jobs stem from tasks in this task set. *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Let [blocking_bound] be a bound on the priority inversion caused by jobs
+      with lower priority. *)
+  Variable blocking_bound: duration -> duration.
+
+  (** The following argument assumes an ideal uniprocessor. *)
+  Hypothesis H_uni : uniprocessor_model PState.
+  Hypothesis H_unit : unit_service_proc_model PState.
+  Hypothesis H_progress : ideal_progress_proc_model PState.
+
+  (** We show that, if the maximum length of a priority inversion of a given job [j]
+      is bounded by the blocking bound,... *)
+  Hypothesis H_priority_inversion_is_bounded_by_blocking:
+    forall j t1 t2,
+      arrives_in arr_seq j ->
+      job_of_task tsk j ->
+      busy_interval_prefix arr_seq sched j t1 t2 ->
+      max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound (job_arrival j - t1).
+
+  (** ... then the priority inversion incurred by any job is bounded by the blocking bound. *)
+  Lemma priority_inversion_is_bounded :
+    priority_inversion_is_bounded_by arr_seq sched tsk blocking_bound.
+  Proof.
+    move=> j ARR TSK POS t1 t2 PREF.
+    move: (PREF) => [_ [_ [_ /andP [T _]]]].
+    move: H_valid_schedule => [COARR MBR].
+    have [NEQ|NEQ] := boolP ((t2-t1) <= blocking_bound (job_arrival j - t1)).
+    { apply leq_trans with (t2 -t1) => [|//].
+      rewrite /cumulative_priority_inversion.
+      rewrite -[X in _ <= X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat.
+      by rewrite leq_sum //; move=> t _; destruct (priority_inversion). }
+    have [ppt [PPT' /andP[GE LE]]]: exists ppt : instant,
+                                      preemption_time arr_seq sched ppt /\
+                                      t1 <= ppt <=
+                                      t1 + max_lp_nonpreemptive_segment arr_seq j t1
+      by exact: preemption_time_exists.
+    apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 ppt).
+    - by apply: priority_inversion_occurs_only_till_preemption_point =>//.
+    - apply leq_trans with (ppt - t1).
+      + rewrite /cumulative_priority_inversion -[X in _ <= X]addn0 -[ppt - t1]mul1n
+                -iter_addn -big_const_nat.
+        by rewrite leq_sum //; move=> t _; case: priority_inversion. 
+      + rewrite leq_subLR.
+        apply leq_trans with (t1 + max_lp_nonpreemptive_segment arr_seq j t1) => [//|].
+        by rewrite leq_add2l; apply: (H_priority_inversion_is_bounded_by_blocking j t1 t2).
+  Qed.
+
+End PriorityInversionIsBounded.

analysis/facts/busy_interval/pi_cond.v

+Require Export prosa.analysis.facts.busy_interval.pi.
+
+(** This file relates the general notion of [cumulative_priority_inversion] with
+    the more specialized notion [cumulative_priority_inversion_cond]. *)
+
+Section CondPI.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{Arrival : JobArrival Job}.
+  Context `{Cost : JobCost Job}.
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
+
+  (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
+  Context {PState : ProcessorState Job}.
+  Hypothesis H_uni : uniprocessor_model PState.
+  Variable sched : schedule PState.
+
+  (** Consider a JLFP policy that indicates a higher-or-equal priority relation,
+      and assume that the relation is reflexive and transitive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
+  Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
+
+  (** Consider a valid preemption model with known maximum non-preemptive
+      segment lengths. *)
+  Context `{TaskMaxNonpreemptiveSegment Task} `{JobPreemptable Job}.
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** Further, allow for any work-bearing notion of job readiness. *)
+  Context `{@JobReady Job PState Cost Arrival}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** We assume that the schedule is valid. *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** Next, we assume that the schedule is a work-conserving schedule... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** ... and the schedule respects the scheduling policy at every preemption point. *)
+  Hypothesis H_respects_policy :
+    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
+
+  (** Consider any job [j] of [tsk] with positive job cost. *)
+  Variable j : Job.
+  Hypothesis H_j_arrives : arrives_in arr_seq j.
+  Hypothesis H_job_cost_positive : job_cost_positive j.
+
+  (** Consider any busy interval prefix <<[t1, t2)>> of job j. *)
+  Variable t1 t2 : instant.
+  Hypothesis H_busy_interval_prefix:
+    busy_interval_prefix arr_seq sched j t1 t2.
+
+  (** We establish a technical rewriting lemma that allows us to replace
+      [cumulative_priority_inversion] with
+      [cumulative_priority_inversion_cond] by exploiting the observation
+      that a single job remains scheduled throughout the interval in which job
+      [j] suffers priority inversion. *)
+  Lemma cum_task_pi_eq :
+    forall (jlp : Job) (P : pred Job),
+      scheduled_at sched jlp t1 ->
+      P jlp ->
+        cumulative_priority_inversion arr_seq sched j t1 t2
+        = cumulative_priority_inversion_cond arr_seq sched j P t1 t2.
+  Proof.
+    move=> jlp P SCHED Pjlp.
+    apply: eq_big_nat => // t /andP [t1t tt2].
+    apply/eqP; rewrite nat_of_bool_eq; apply/eqP/andb_id2l => NSCHED.
+    have suff: forall j',
+        j' \in scheduled_jobs_at arr_seq sched t ->
+        ~~ hep_job j' j ->
+        P j'.
+    { move=> SUFF.
+      apply: eq_in_has => j' => SCHED'.
+      have [_|NHEP] := boolP (hep_job j' j); first by rewrite andFb.
+      by rewrite andTb SUFF. }
+    { apply => j' SCHED' NHEP.
+      move: SCHED'; rewrite scheduled_jobs_at_iff // => SCHED''.
+      have PI: priority_inversion arr_seq sched j t by apply /uni_priority_inversion_P.
+      have j't1: scheduled_at sched j' t1
+        by apply: (pi_job_remains_scheduled arr_seq) =>//; apply /andP.
+      have -> // : j' = jlp.
+      { apply /eqP/contraT => NEQ; move: SCHED; apply /contraLR => _.
+        by apply scheduled_job_at_neq with (j:= j'). } }
+  Qed.
+
+End CondPI.

analysis/facts/busy_interval/quiet_time.v

+Require Export prosa.analysis.definitions.busy_interval.classical.
+Require Export prosa.analysis.definitions.carry_in.
+
+(** In this module we collect some basic facts about quiet times. *)
+
+Section Facts.
+
+  (** Consider any kind of jobs... *)
+  Context {Job : JobType} `{JobArrival Job} `{JobCost Job}.
+  (** ... and a [JLFP] policy defined on these jobs. *)
+  Context `{JLFP_policy Job}.
+  (** Consider any processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any schedule and arrival sequence. *)
+  Variable sched : schedule PState.
+  Variable arr_seq : arrival_sequence Job.
+
+  (** We prove that 0 is always a quiet time. *)
+  Lemma zero_is_quiet_time (j : Job) :
+    quiet_time arr_seq sched j 0.
+  Proof. by move=> jhp ARR HP; rewrite /arrived_before ltn0. Qed.
+
+  (** The fact that there is no carry-in at time instant [t] trivially
+      implies that [t] is a quiet time. *)
+  Lemma no_carry_in_implies_quiet_time :
+    forall j t,
+      no_carry_in arr_seq sched t ->
+      quiet_time arr_seq sched j t.
+  Proof. by move=> j t + j_hp ARR HP BEF; apply. Qed.
+
+  (** For convenience in proofs, we restate that by definition there are no
+      quiet times in a busy-interval prefix... *)
+  Fact busy_interval_prefix_no_quiet_time :
+    forall j t1 t2,
+      busy_interval_prefix arr_seq sched j t1 t2 ->
+      (forall t, t1 < t < t2 -> ~ quiet_time arr_seq sched j t).
+  Proof. by move=> j t1 t2 [_ [_ [NQT _]]]. Qed.
+
+  (** ... and hence also not in a busy interval. *)
+  Fact busy_interval_no_quiet_time :
+    forall j t1 t2,
+      busy_interval arr_seq sched j t1 t2 ->
+      (forall t, t1 < t < t2 -> ~ quiet_time arr_seq sched j t).
+  Proof. by move=> j t1 t2 [BIP _]; exact: busy_interval_prefix_no_quiet_time. Qed.
+
+End Facts.

analysis/facts/busy_interval/service_inversion.v

+Require Export prosa.analysis.definitions.service_inversion.busy_prefix.
+Require Export prosa.analysis.facts.busy_interval.pi.
+
+
+(** * Service Inversion Lemmas *)
+(** In this section, we prove a few lemmas about service inversion. *)
+Section ServiceInversion.
+
+  (** Consider any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of fully supply-consuming uniprocessor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any arrival sequence with consistent, non-duplicate arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any uni-processor schedule of this arrival sequence... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence :
+    jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival or after
+      completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** In this section, we prove a few basic lemmas about priority inversion. *)
+  Section BasicLemmas.
+
+    (** Consider an JLDP policy that indicates a higher-or-equal
+        priority relation, and assume that the relation is
+        reflexive. *)
+    Context {JLDP : JLDP_policy Job}.
+    Hypothesis H_priority_is_reflexive : reflexive_priorities JLDP.
+
+    (** First, we show that a blackout at a time instant [t] implies
+        that there is no service inversion at time [t]. *)
+    Lemma blackout_implies_no_service_inversion :
+      forall (j : Job) (t : instant),
+        is_blackout sched t ->
+        ~~ service_inversion arr_seq sched j t.
+    Proof.
+      move=> j t SUP.
+      apply/negP => /andP [_ /hasP [s IN LP]].
+      move: (SUP) => /negP NSUP; apply: NSUP.
+      by apply: receives_service_implies_has_supply.
+    Qed.
+
+    (** Similarly, there is no service inversion at an idle time instant. *)
+    Lemma idle_implies_no_service_inversion :
+      forall (j : Job) (t : instant),
+        is_idle arr_seq sched t ->
+        ~~ service_inversion arr_seq sched j t.
+    Proof.
+      move=> j t IDLE; rewrite /service_inversion.
+      rewrite negb_and negbK; apply/orP; right.
+      apply/hasPn => [s A].
+      apply served_at_and_receives_service_consistent in A.
+      exfalso.
+      by apply/negP; first apply: no_service_received_when_idle => //.
+    Qed.
+
+    (** Next, we prove that if a job [j] receives service at time [t],
+        job [j] does not incur service inversion at time [t].  *)
+    Lemma receives_service_implies_no_service_inversion :
+      forall (j : Job) (t : instant),
+        receives_service_at sched j t ->
+        ~~ service_inversion arr_seq sched j t.
+    Proof.
+      move=> j t RSERV; apply/negP => /andP [_ /hasP [s IN LP]].
+      have EQ: j = s by apply: only_one_job_receives_service_at_uni => //.
+      subst; move: LP => /negP NHEP; apply: NHEP.
+      by apply H_priority_is_reflexive.
+    Qed.
+
+    (** We show that cumulative service inversion received during an
+        interval <<[t1, t2)>> can be split into the sum of cumulative
+        service inversion <<[t1, t)>> and <<[t, t2)>> for any <<t2 \in
+        [t1, t3]>>.  *)
+    Lemma service_inversion_cat :
+      forall (j : Job) (t1 t2 t : instant),
+        t1 <= t ->
+        t <= t2 ->
+        cumulative_service_inversion arr_seq sched j t1 t2
+        = cumulative_service_inversion arr_seq sched j t1 t
+          + cumulative_service_inversion arr_seq sched j t t2.
+    Proof. by move=> j t1 t2 t LE1 LE2; rewrite -big_cat_nat //=. Qed.
+
+    (** Next, we show that cumulative service inversion on an interval
+        <<[al, ar)>> is bounded by the cumulative service inversion on
+        an interval <<[bl,br)>> if <<[al,ar)>> ⊆ <<[bl,br)>>. *)
+    Lemma service_inversion_widen :
+      forall (j : Job) (al ar bl br : instant),
+        bl <= al ->
+        ar <= br ->
+        cumulative_service_inversion arr_seq sched j al ar
+        <= cumulative_service_inversion arr_seq sched j bl br.
+    Proof.
+      move=> j al ar bl br LE1 LE2.
+      rewrite /cumulative_service_inversion.
+      have [NEQ1|NEQ1] := leqP al ar; last by rewrite big_geq //.
+      rewrite (big_cat_nat _ _ _ LE1) //=; last by lia.
+      by rewrite (big_cat_nat _ _ _ _ LE2) //= addnC -addnA leq_addr //=.
+    Qed.
+
+  End BasicLemmas.
+
+  (** In the following section, we prove one rewrite rule about
+      service inversion. *)
+  Section ServiceInversionRewrite.
+
+    (** Consider a reflexive JLDP policy. *)
+    Context {JLDP : JLDP_policy Job}.
+    Hypothesis H_priority_is_reflexive : reflexive_priorities JLDP.
+
+    (** Consider a time instant [t] ... *)
+    Variable t : instant.
+
+    (** ... and assume that there is supply at [t]. *)
+    Hypothesis H_supply : has_supply sched t.
+
+    (** Consider two (not necessarily distinct) jobs [j] and [j'] and
+        assume that job [j] is scheduled at time [t]. *)
+    Variables j j' : Job.
+    Hypothesis H_sched : scheduled_at sched j t.
+
+    (** Then the predicate "is there service inversion for job [j'] at
+        time [t]?" is equal to the predicate "is job [j] has lower
+        priority than job [j']?" *)
+    Lemma service_inversion_supply_sched :
+      service_inversion arr_seq sched j' t = ~~ hep_job_at t j j'.
+    Proof.
+      have RSERV : receives_service_at sched j t by apply ideal_progress_inside_supplies.
+      apply/idP/idP.
+      { move => /andP [IN /hasP [s SE LP]].
+        have EQj: s = j by apply: only_one_job_receives_service_at_uni.
+        by subst. }
+      { move => NHEP; apply/andP; split.
+        - move: NHEP; apply contra => SERV.
+          have EQj: j = j' by apply: only_one_job_receives_service_at_uni.
+          by subst; apply H_priority_is_reflexive.
+        - apply/hasP; exists j => //.
+          by apply: receives_service_and_served_at_consistent. }
+    Qed.
+
+  End ServiceInversionRewrite.
+
+  (** In the last section, we prove that cumulative service inversion
+      is bounded by cumulative priority inversion. *)
+  Section PriorityInversion.
+
+    (** Consider a reflexive JLFP policy.
+
+        Note that, unlike the other sections, this section assumes a
+        JLFP policy. This is due to the fact that priority inversion
+        is defined in terms of JLFP policies. This is not a
+        fundamental assumption and may be relaxed in the future. *)
+    Context {JLFP : JLFP_policy Job}.
+    Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
+
+    (** We prove that service inversion implies priority inversion ... *)
+    Lemma service_inv_implies_priority_inv :
+      forall (j : Job) (t : instant),
+        service_inversion arr_seq sched j t ->
+        priority_inversion arr_seq sched j t.
+    Proof.
+      move=> j t.
+      move=> /andP [NSERV /hasP [s IN LP]]; apply/andP; split.
+      { apply/negP => INj; rewrite scheduled_jobs_at_iff in INj => //.
+        have EQ : s = j.
+        { apply: H_uniprocessor_proc_model => //.
+          by eapply service_at_implies_scheduled_at, served_at_and_receives_service_consistent. }
+        by subst; move: LP => /negP LP; apply: LP; apply H_priority_is_reflexive. }
+      { apply/hasP; exists s => //.
+        rewrite scheduled_jobs_at_iff => //.
+        by apply service_at_implies_scheduled_at; apply: served_at_and_receives_service_consistent. }
+    Qed.
+
+    (** ... and, as a corollary, it is easy to see that cumulative
+        service inversion is bounded by cumulative priority
+        inversion. *)
+    Corollary cumul_service_inv_le_cumul_priority_inv :
+      forall (j : Job) (t1 t2 : instant),
+        cumulative_service_inversion arr_seq sched j t1 t2
+        <= cumulative_priority_inversion arr_seq sched j t1 t2.
+    Proof.
+      move=> j t1 t2; apply leq_sum => t _.
+      have L : forall (a b : bool), (a -> b) -> a <= b by clear; move => [] [].
+      by apply L, service_inv_implies_priority_inv.
+    Qed.
+
+  End PriorityInversion.
+
+End ServiceInversion.
+
+(** In the following, we prove that the cumulative service inversion
+    in a busy interval prefix is bounded. *)
+Section ServiceInversionIsBounded.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of fully supply-consuming unit-supply
+      uniprocessor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider an JLFP policy that indicates a higher-or-equal priority
+      relation, and assume that the relation is reflexive and
+      transitive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
+  Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
+
+  (** Consider any arrival sequence with consistent, non-duplicate arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any uni-processor schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Next, allow for any work-bearing notion of job readiness ... *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** ... and assume that the schedule is valid.  *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** In addition, we assume the existence of a function mapping jobs
+      to their preemption points ... *)
+  Context `{JobPreemptable Job}.
+
+  (** ... and assume that it defines a valid preemption model with
+      bounded non-preemptive segments. *)
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (**  Next, we assume that the schedule respects the scheduling policy. *)
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
+
+  (** In the following section, we prove that cumulative service
+      inversion in a busy-interval prefix is necessarily caused by one
+      lower-priority job. *)
+  Section CumulativeServiceInversionFromOneJob.
+
+    (** Consider any job [j] with a positive job cost. *)
+    Variable j : Job.
+    Hypothesis H_j_arrives : arrives_in arr_seq j.
+    Hypothesis H_job_cost_positive : job_cost_positive j.
+
+    (** Let <[t1, t2)>> be a busy-interval prefix. *)
+    Variable t1 t2 : instant.
+    Hypothesis H_busy_prefix : busy_interval_prefix arr_seq sched j t1 t2.
+
+    (** Consider a time instant [t : t <= t2] such that ... *)
+    Variable t : instant.
+    Hypothesis H_t_le_t2 : t <= t2.
+
+    (** ... the cumulative service inversion is positive in <<[t1, t)>>. *)
+    Hypothesis H_service_inversion_positive : 0 < cumulative_service_inversion arr_seq sched j t1 t.
+
+    (** First, note that there is a lower-priority job that receives
+        service at some time during the time interval <<[t1, t)>>. *)
+    Local Lemma lower_priority_job_receives_service :
+      exists (jlp : Job) (to : instant),
+        t1 <= to < t
+        /\ ~~ hep_job jlp j
+        /\ receives_service_at sched jlp to.
+    Proof.
+      move: H_service_inversion_positive; rewrite sum_nat_gt0 filter_predT => /hasP [t' IN POS].
+      rewrite mem_index_iota in IN; rewrite lt0b in POS.
+      move: POS => /andP [NIN /hasP [jlp INlp LP]].
+      exists jlp, t'.
+      by rewrite IN LP.
+    Qed.
+
+    (** Then we prove that the service inversion incurred by job [j]
+        can only be caused by _one_ lower priority job. *)
+    Lemma cumulative_service_inversion_from_one_job :
+      exists (jlp : Job),
+        job_arrival jlp < t1
+        /\ ~~ hep_job jlp j
+        /\ cumulative_service_inversion arr_seq sched j t1 t = service_during sched jlp t1 t.
+    Proof.
+      have [jlp [to [NEQ [LP SERV]]]] := lower_priority_job_receives_service.
+      exists jlp; split; last split => //.
+      - apply: low_priority_job_arrives_before_busy_interval_prefix => //=.
+        + by instantiate (1 := to); lia.
+        + by apply service_at_implies_scheduled_at.
+      - apply: eq_sum_seq => t'; rewrite mem_index_iota => NEQt' _.
+        have [ZERO | POS] := unit_supply_proc_service_case H_unit_supply_proc_model sched jlp t'.
+        + rewrite ZERO eqb0; apply/negP => /andP [_ /hasP [joo SERVoo LPoo]].
+          have EQ : jlp = joo.
+          { apply: only_one_pi_job => //=.
+            * by instantiate (1 := to); lia.
+            * by apply service_at_implies_scheduled_at.
+            * by instantiate (1 := t'); lia.
+            * apply: service_at_implies_scheduled_at.
+              by apply: served_at_and_receives_service_consistent.
+          }
+          subst joo.
+          apply served_at_and_receives_service_consistent in SERVoo.
+          by move: SERVoo; rewrite /receives_service_at ZERO.
+        + rewrite POS eqb1; apply/andP; split.
+          * apply/negP => IN; apply served_at_and_receives_service_consistent in IN.
+            have EQ: j = jlp by apply: only_one_job_receives_service_at_uni => //; rewrite /receives_service_at.
+            by subst jlp; move: LP => /negP LP; apply: LP; apply H_priority_is_reflexive. 
+          * apply/hasP; exists jlp; last by apply: LP.
+            apply receives_service_and_served_at_consistent => //.
+            by rewrite /receives_service_at POS.
+    Qed.
+
+  End CumulativeServiceInversionFromOneJob.
+
+  (** In this section, we prove that, given a job [j] with a busy
+      interval prefix <<[t1, t2)>> and a lower-priority job [jlp], the
+      service of [jlp] within the busy interval prefix is bounded by
+      the maximum non-preemptive segment of job [jlp]. *)
+  Section ServiceOfLowPriorityJobIsBounded.
+
+    (** Consider an arbitrary job [j] with positive cost ... *)
+    Variable j : Job.
+    Hypothesis H_j_arrives : arrives_in arr_seq j.
+    Hypothesis H_j_job_cost_positive : job_cost_positive j.
+
+    (** ... and a lower-priority job [jlp]. *)
+    Variable jlp : Job.
+    Hypothesis H_jlp_arrives : arrives_in arr_seq jlp.
+    Hypothesis H_jlp_lp : ~~ hep_job jlp j.
+
+    (** Let <<[t1, t2)>> be a busy interval prefix of job [j]. *)
+    Variable t1 t2 : instant.
+    Hypothesis H_busy_prefix : busy_interval_prefix arr_seq sched j t1 t2.
+
+    (** First, we consider a scenario when there is no preemption time
+        inside of the busy interval prefix _but_ there is a time
+        instant where [jlp] is scheduled. In this case, the cumulative
+        service inversion of job [j] in the time interval <<[t1, t2)>>
+        is bounded by the total service of job [jlp] received in the
+        interval <<[t1, t2)>>. *)
+    Local Lemma no_preemption_impl_service_inv_bounded :
+      (forall t, t1 <= t < t2 -> ~~ preemption_time arr_seq sched t) ->
+      (exists t, t1 <= t < t2 /\ scheduled_at sched jlp t) ->
+      cumulative_service_inversion arr_seq sched j t1 t2 <= service_during sched jlp t1 t2.
+    Proof.
+      move=> NPT SCHED.
+      rewrite [leqLHS]big_seq [leqRHS]big_seq; apply leq_sum => t.
+      rewrite mem_index_iota => /andP [LE LT].
+      have F : forall (b : bool) (n : nat), (b -> 0 < n) -> b <= n by lia.
+      apply: F => /andP [ZE /hasP [h IN LPh]].
+      have EQ: h = jlp; last by subst; apply: served_at_and_receives_service_consistent.
+      apply: H_uniprocessor_proc_model.
+      { by apply served_at_and_receives_service_consistent in IN; apply: service_at_implies_scheduled_at. }
+      { move: SCHED => [t' [/andP [LE' LT'] SCHED]].
+        unshelve apply: neg_pt_scheduled_continuous => //.
+        - by generalize dependent t'; clear; lia.
+        - by generalize dependent t; clear; lia.
+      }
+    Qed.
+
+    (** In this section, we assume that [jlp] is scheduled inside of
+        the busy interval prefix and prove that its service is bounded
+        by [jlp]'s maximum non-preemptive segment. *)
+    Section ServiceOfLPJobIsBounded.
+
+      (** Consider an arbitrary time instant [t] such that [t <= t2]. *)
+      Variables t : instant.
+      Hypothesis H_t_le_t2 : t <= t2.
+
+      (** Consider a second time instant [st] such that [t1 <= st < t]
+          and [jlp] is scheduled at time [st]. *)
+      Variable st : instant.
+      Hypothesis H_t1_le_st_lt_t : t1 <= st < t.
+      Hypothesis H_jlp_sched : scheduled_at sched jlp st.
+
+      (** Consider a preemption point [σ] of job [jlp] such that ... *)
+      Variable σ : duration.
+      Hypothesis H_σ_is_pt : job_preemptable jlp σ.
+
+      (** ... [σ] is greater than or equal to the service of [jlp] at
+          time [t1] but exceeds the service by at most
+          [job_max_nonpreemptive_segment jlp - ε]. *)
+      Hypothesis H_σ_constrained :
+        service sched jlp t1
+        <= σ
+        <= service sched jlp t1 + (job_max_nonpreemptive_segment jlp - ε).
+
+      (** Next, we perform case analysis on whether job [jlp] has
+          reached [σ] units of service by time [t]. *)
+
+      (** First, assume that the service of [jlp] at time [t] is
+          smaller than [σ]. In this case, it is easy to see from the
+          hypothesis [H_σ_constrained] that the service received by
+          [jlp] within time interval <<[t1, t)>> is bounded by
+          [job_max_nonpreemptive_segment jlp - ε]. *)
+      Local Lemma small_service_implies_bounded_service :
+        service sched jlp t < σ ->
+        service_during sched jlp t1 t <= job_max_nonpreemptive_segment jlp - ε.
+      Proof.
+        move => B; move_neq_up CO.
+        have E : σ <= service sched jlp t1 + service_during sched jlp t1 t by lia.
+        by move: B E; rewrite service_cat /service; lia.
+      Qed.
+
+      (** Next, assume that [σ <= service sched jlp t]. In this case,
+          we can show that [jlp] is preempted after it reaches [σ]
+          units of service and hence, again, the service during <<[t1,
+          t)>> is bounded by [job_max_nonpreemptive_segment jlp - ε]. *)
+      Local Lemma big_service_implies_bounded_service :
+        σ <= service sched jlp t ->
+        service_during sched jlp t1 t <= job_max_nonpreemptive_segment jlp - ε.
+      Proof.
+        rewrite -[service_during _ _ _ _ <= _](leq_add2l (service sched jlp t1)).
+        rewrite leq_eqVlt => /orP [/eqP EQ|GT].
+        { by rewrite service_cat; [ rewrite -EQ; move: H_σ_constrained => /andP [A B] | lia]. }
+        exfalso.
+        have [pt [LTpt EQ]] : exists pt, pt < t /\ service sched jlp pt = σ.
+        { by apply exists_intermediate_service => //; apply unit_supply_is_unit_service. }
+        have NPT : ~~ preemption_time arr_seq sched t1.
+        { by eapply lower_priority_job_scheduled_implies_no_preemption_time
+          with (t1 := t1) (t2:= t2) (t := st) (jlp := jlp) (j := j)=> //; lia. }
+        have LEpt: t1 <= pt.
+        { move_neq_up LEpt.
+          have EQ1: service sched jlp t1 = σ.
+          { apply/eqP; rewrite eqn_leq; apply/andP; split;
+              first by move: H_σ_constrained => /andP [A B].
+            by rewrite -EQ; apply: service_monotonic; lia. }
+          have PT :  preemption_time arr_seq sched t1.
+          { rewrite /preemption_time.
+            have ->: scheduled_job_at arr_seq sched t1 = Some jlp.
+            { apply/eqP; rewrite scheduled_job_at_scheduled_at => //.
+              eapply lower_priority_job_continuously_scheduled
+                with (t1 := t1) (t2:= t2) (t := st) (jlp := jlp) (j := j)=> //=; lia. }
+            by rewrite EQ1.
+          }
+          by rewrite PT in NPT. }
+        have [t' [NEQ' [SERV' SCHED']]] := kth_scheduling_time sched _ _ _ _ EQ GT.
+        have PT : preemption_time arr_seq sched t'.
+        { move: SCHED'; erewrite <-scheduled_job_at_scheduled_at => //.
+          by rewrite /preemption_time; move => /eqP ->; rewrite SERV'. }
+        move: H_jlp_lp => /negP LP2; apply: LP2.
+        apply: scheduled_at_preemption_time_implies_higher_or_equal_priority => //.
+        by move: NEQ' LEpt H_t_le_t2; clear; lia.
+      Qed.
+
+      (** Either way, the service of job [jlp] during the time
+          interval <<[t1, t)>> is bounded by
+          [job_max_nonpreemptive_segment jlp - ε]. *)
+      Local Lemma lp_job_bounded_service_aux :
+        service_during sched jlp t1 t <= job_max_nonpreemptive_segment jlp - ε.
+      Proof.
+        have [B|S] := leqP σ (service sched jlp t); last first.
+        - by apply small_service_implies_bounded_service.
+        - by apply big_service_implies_bounded_service.
+      Qed.
+
+    End ServiceOfLPJobIsBounded.
+
+    (** Note that the preemption point [σ] assumed in the previous
+        section always exists. *)
+    Local Remark preemption_point_of_jlp_exists :
+      exists σ,
+        service sched jlp t1 <= σ <= service sched jlp t1 + (job_max_nonpreemptive_segment jlp - ε)
+        /\ job_preemptable jlp σ.
+    Proof.
+      move: (proj2 (H_valid_model_with_bounded_nonpreemptive_segments) jlp H_jlp_arrives) =>[_ EXPP].
+      have T: 0 <= service sched jlp t1 <= job_cost jlp.
+      { by apply/andP; split=> [//|]; apply service_at_most_cost, unit_supply_is_unit_service => //. }
+      by move: (EXPP (service sched jlp t1) T) => [pt [NEQ2 PP]]; exists pt.
+    Qed.
+
+    (** We strengthen the lemma [lp_job_bounded_service_aux] by
+        removing the assumption that [jlp] is scheduled somewhere in
+        the busy interval prefix. *)
+    Lemma lp_job_bounded_service :
+      forall t,
+        t <= t2 ->
+        service_during sched jlp t1 t <= job_max_nonpreemptive_segment jlp - ε.
+    Proof.
+      move=> t LT.
+      have [ZE|POS] := posnP (service_during sched jlp t1 t); first by rewrite ZE.
+      have [st [NEQ SCHED]] := cumulative_service_implies_scheduled _ _ _ _ POS.
+      have [σ [EX PTσ]] := preemption_point_of_jlp_exists.
+      by apply: lp_job_bounded_service_aux.
+    Qed.
+
+    (** Finally, we remove [jlp] from the RHS of the inequality by
+        taking the maximum over all jobs that arrive before time [t1]. *)
+    Lemma lp_job_bounded_service_max :
+      forall t,
+        t <= t2 ->
+        service_during sched jlp t1 t <= max_lp_nonpreemptive_segment arr_seq j t1.
+    Proof.
+      move=> t LT.
+      have [ZE|POS] := posnP (service_during sched jlp t1 t); first by rewrite ZE.
+      have [st [NEQ SCHED]] := cumulative_service_implies_scheduled _ _ _ _ POS.
+      rewrite (leqRW (lp_job_bounded_service _ _)) //.
+      rewrite /max_lp_nonpreemptive_segment -(leqRW (leq_bigmax_cond_seq _ _ _ jlp _ _)) //.
+      { apply: arrived_between_implies_in_arrivals => //.
+        apply/andP; split => //.
+        by (apply: low_priority_job_arrives_before_busy_interval_prefix; try apply: H_busy_prefix) => //; lia.
+      }
+      { by rewrite H_jlp_lp andTb; apply: scheduled_implies_positive_cost. }
+    Qed.
+
+  End ServiceOfLowPriorityJobIsBounded.
+
+  (** Let [tsk] be any task to be analyzed. *)
+  Variable tsk : Task.
+
+  (** Let [blocking_bound] be a bound on the maximum length of a
+      nonpreemptive segment of a lower-priority job. *)
+  Variable blocking_bound : duration -> duration.
+
+  (** We show that, if the maximum length of a nonpreemptive segment
+      is bounded by the blocking bound, ... *)
+  Hypothesis H_priority_inversion_is_bounded_by_blocking :
+    forall j t1 t2,
+      arrives_in arr_seq j ->
+      job_of_task tsk j ->
+      busy_interval_prefix arr_seq sched j t1 t2 ->
+      max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound (job_arrival j - t1).
+
+  (** ... then the service inversion incurred by any job is bounded by
+      the blocking bound. *)
+  Lemma service_inversion_is_bounded :
+    service_inversion_is_bounded_by arr_seq sched tsk blocking_bound.
+  Proof.
+    move=> j ARR TSK POS t1 t2 BUSY.
+    rewrite -(leqRW (H_priority_inversion_is_bounded_by_blocking _ _ _ _ _ _ )) //.
+    edestruct busy_interval_pi_cases as [CPI|PI]; (try apply BUSY) => //.
+    { by rewrite (leqRW (cumul_service_inv_le_cumul_priority_inv _ _  _ _ _ _ _ _ _ _)) //. }
+    { move: (PI) => /andP [_ /hasP [jlp INjlp LPjlp]].
+      have SCHEDjlp : scheduled_at sched jlp t1 by erewrite <-scheduled_jobs_at_iff => //.
+      have [NPT| [pt [/andP [LE1 LE2] [PT MIN]]]] := preemption_time_interval_case arr_seq sched t1 t2.
+      { rewrite (leqRW (no_preemption_impl_service_inv_bounded j _ jlp _ _ _ _ _ )) //.
+        - by apply: lp_job_bounded_service_max.
+        - by exists t1; split => //; apply/andP; split; [ | move: BUSY => [T _]]; lia. }
+      { have LEQ : cumulative_service_inversion arr_seq sched j t1 t2
+                   <= cumulative_service_inversion arr_seq sched j t1 pt.
+        { have [LE|WF] := leqP t2 pt.
+          { by rewrite (leqRW (service_inversion_widen arr_seq sched j t1 _ _ pt _ _ )) => //. }
+          { rewrite (service_inversion_cat _ _ _ _ _ pt) //
+                    -{2}[_ _ _ j t1 pt]addn0 leq_add2l
+                    (leqRW (cumul_service_inv_le_cumul_priority_inv _ _ _ _ _ _ _ _ _ _))//  leqn0.
+            rewrite /cumulative_priority_inversion big_nat_cond; apply/eqP; apply big1 => t /andP [NEQ3 _]; apply/eqP.
+            by rewrite eqb0; apply: no_priority_inversion_after_preemption_point => //; lia. } }
+        rewrite (leqRW LEQ) (leqRW (no_preemption_impl_service_inv_bounded j _ jlp _ _ _ _ _ )) //; clear LEQ.
+        { by apply: lp_job_bounded_service_max => //; lia. }
+        { move=> t /andP [NEQ1 NEQ2]; apply/negP => PTt.
+          by specialize (MIN _ NEQ1 PTt); move: MIN NEQ2; clear; lia. }
+        { exists t1; split => //.
+          apply/andP; split => //.
+          move_neq_up LE; have EQ: pt = t1; [by lia | subst].
+          eapply no_preemption_time_before_pi with (t := t1) in PI => //.
+          - by rewrite PT in PI.
+          - by move: LE2; clear; lia.
+          - by clear; lia. }
+      }
+    }
+  Qed.
+
+End ServiceInversionIsBounded.

analysis/facts/delay_propagation.v

+Require Export prosa.analysis.definitions.delay_propagation.
+Require Export prosa.analysis.facts.behavior.arrivals.
+
+(** *  Propagation of Delays in Arrival Curves *)
+
+(** In this module, we prove properties of the generic delay propagation
+    definitions provided in [prosa.analysis.definitions.delay_propagation]. *)
+
+Section ACPropFacts.
+
+  (** Consider two kinds of tasks... *)
+  Context {Task1 Task2 : TaskType}.
+
+  (** ... and their associated kinds of jobs. *)
+  Context {Job1 Job2 : JobType}
+    `{JobTask Job1 Task1} `{JobTask Job2 Task2}
+    (JA1 : JobArrival Job1) (JA2 : JobArrival Job2).
+
+  (** Suppose we are given a mapping of jobs (resp., tasks) of the second kind
+      to jobs (resp., tasks) of the first kind. *)
+  Variable job1_of : Job2 -> Job1.
+  Variable task1_of : Task2 -> Task1.
+
+  (** Furthermore, suppose we also have a reverse mapping from jobs of the first
+      kind to the associated jobs of the second kind. *)
+  Variable job2_of : Job1 -> seq Job2.
+
+  (** The relation of the jobs is as follows: a job [j2 : Job2] arrives exactly
+      [arrival_delay j2] time units after the arrival of its corresponding job
+      [job1_of j2], where the maximum possible delay is bounded by [delay_bound
+      (job_task j2)]. *)
+  Variable arrival_delay : Job2 -> duration.
+  Variable delay_bound : Task2 -> duration.
+
+  (** Consider any set of type-two tasks. *)
+  Variable ts2 : seq Task2.
+
+  (** If the mapping of type-two tasks to type-one tasks is valid for the tasks
+      in the considered task set, ... *)
+  Hypothesis H_valid_mapping :
+    valid_delay_propagation_mapping
+      JA1 JA2 job1_of task1_of delay_bound ts2.
+
+  (** ... and we are given an arrival curve for the first kind of tasks, ... *)
+  Context {max_arrivals1 : MaxArrivals Task1}.
+
+  (** ... then we obtain a derived (or propagated) arrival curve for tasks of
+      the second kind.  *)
+  #[local] Instance  max_arrivals2 : MaxArrivals Task2 :=
+    propagated_arrival_curve task1_of delay_bound.
+
+  (** Additionally, given an arbitrary arrival sequence of type-one jobs, *)
+  Variable arr_seq1 : arrival_sequence Job1.
+
+  (** ... if the mapping of type-two jobs to type-one jobs is valid, ... *)
+  Hypothesis H_arr_seq_mapping :
+    valid_arr_seq_propagation_mapping
+      JA1 JA2 job1_of delay_bound arr_seq1 job2_of arrival_delay ts2.
+
+  (** ... it induces a derived arrival sequence of type-two jobs.  *)
+  Let arr_seq2 := propagated_arrival_sequence JA1 job1_of arr_seq1 job2_of arrival_delay.
+
+  (** ** Arrival Sequence Validity Properties *)
+
+  (** In the following, we establish that the derived arrival sequence is
+      structurally valid. *)
+
+  (** First, the induced arrival sequence is consistent with the arrival times
+      of type-two jobs. *)
+  Lemma consistent_propagated_arrival_sequence :
+    consistent_arrival_times arr_seq2.
+  Proof.
+    move=> j2 t.
+    rewrite /arrives_at/arrivals_at/arr_seq2/propagated_arrival_sequence.
+    rewrite mem_filter => /andP[/eqP <- _].
+    by move: H_arr_seq_mapping => [_ _ _ {}].
+  Qed.
+
+  (** Second, the induced arrival sequence does not duplicate any jobs. *)
+  Lemma propagated_arrival_sequence_uniq :
+    valid_arrival_sequence arr_seq1 ->
+    arrival_sequence_uniq arr_seq2.
+  Proof.
+    move=> VALID t.
+    rewrite /arrivals_at/arr_seq2/propagated_arrival_sequence.
+    apply: filter_uniq.
+    rewrite /flatten foldrE big_map big_seq.
+    apply: bigcat_uniq.
+    - move=> j1 IN.
+      move: H_arr_seq_mapping => [_ UNIQ _ _]; apply UNIQ.
+      apply: in_arrivals_implies_arrived.
+      exact: IN.
+    - move=> j2 j1 j1'.
+      move: H_arr_seq_mapping => [CON _ _ _].
+      by rewrite !CON => -> ->.
+    - by apply: arrivals_uniq.
+  Qed.
+
+  (** Taken together, the above two lemmas imply that the derived arrival
+      sequence is valid if the reference arrival sequence is valid. *)
+  Corollary valid_propagated_arrival_sequence :
+    valid_arrival_sequence arr_seq1 ->
+    valid_arrival_sequence arr_seq2.
+  Proof.
+    split; first exact: consistent_propagated_arrival_sequence.
+    exact: propagated_arrival_sequence_uniq.
+  Qed.
+
+  (** A job of the second kind [j2 : Job2] is part of the derived arrival
+      sequence if its associated job of the first kind [job1_of j2] is part of
+      the given reference arrival sequence. *)
+  Lemma arrives_in_propagated_if :
+    forall j2,
+      consistent_arrival_times arr_seq1 ->
+      arrives_in arr_seq1 (job1_of j2) -> arrives_in arr_seq2 j2.
+  Proof.
+    move=> j2 CAT1 IN; move: (IN) => [t IN'].
+    exists (t + arrival_delay j2).
+    rewrite /arrivals_at/arr_seq2/propagated_arrival_sequence.
+    rewrite mem_filter; apply/andP; split;
+      first by rewrite (CAT1 _ t).
+    apply/flatten_mapP.
+    exists (job1_of j2).
+    - apply: job_in_arrivals_between => //.
+      by rewrite (CAT1 _ t) //; lia.
+    - by move: H_arr_seq_mapping => [-> _].
+  Qed.
+
+  (** Conversely, a job of the second kind [j2 : Job2] is part of the derived
+      arrival sequence _only if_ its associated job of the first kind [job1_of
+      j2] is part of the given reference arrival sequence. *)
+  Lemma arrives_in_propagated_only_if :
+    forall j2,
+      arrives_in arr_seq2 j2 -> arrives_in arr_seq1 (job1_of j2).
+  Proof.
+    move=> j2 [t2 {}].
+    rewrite /arrivals_at/arr_seq2/propagated_arrival_sequence.
+    rewrite mem_filter => /andP[/eqP DEF /flatten_mapP[j1 IN1 {}]].
+    move: H_arr_seq_mapping => [-> _ _ _] ->.
+    by apply/in_arrivals_implies_arrived/IN1.
+  Qed.
+
+
+  (** ** Correctness of the Propagated Arrival Curve *)
+
+  (** Next, we establish the correctness of the propagated arrival curve. *)
+
+  (** To this end, we first observe that the defined function satisfies the
+      structural requirements for arrival curves. *)
+  Lemma propagated_arrival_curve_valid :
+    (forall tsk2, tsk2 \in ts2 -> monotone leq (@max_arrivals Task1 max_arrivals1 (task1_of tsk2))) ->
+    valid_taskset_arrival_curve ts2 max_arrivals2.
+  Proof.
+    move=> MONO tsk2 IN2.
+    split => // delta1 delta2 LEQ.
+    case: delta1 LEQ; case: delta2 => //= delta2 delta1 LEQ.
+    apply: MONO => //.
+    by lia.
+  Qed.
+
+  (** In the following, let [ts1] denote the set of type-one tasks that the
+      type-two tasks in [ts2] are mapped to (by [task1_of]). *)
+  Let ts1 := [seq task1_of tsk2 | tsk2 <- ts2].
+
+  (** To establish correctness, we make the assumption that each job of the
+      first kind has at most one associated job of the second kind.
+
+      Generalizations to multiple successors are possible, but the current
+      definition of [propagated_arrival_curve] works only under this
+      restriction. *)
+  Hypothesis H_job2_of_singleton :
+    (forall tsk1,
+        tsk1 \in ts1 -> forall j1,
+            job_task j1 = tsk1 ->
+            size (job2_of j1) <= 1).
+
+  (** Suppose the given type-one arrival sequence and arrival curve are
+      valid. *)
+  Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq1.
+  Hypothesis H_valid_ac : valid_taskset_arrival_curve ts1 max_arrivals1.
+
+  (** In preparation of the correctness argument, we next establish a couple of
+      "stepping stone" lemmas that sketch the main thrust of the correctness
+      argument. *)
+  Section ArrivalCurveCorrectnessSteps.
+
+    (** Consider an interval <<[t1, t2)>> ... *)
+    Variable t1 t2 : instant.
+    Hypothesis H_ordered : t1 <= t2.
+
+    (** ... and any type-two task in the given task set.  *)
+    Variable tsk2 : Task2.
+    Hypothesis H_in_ts : tsk2 \in ts2.
+
+    (** Let [tsk2_arrivals] denote the jobs of [tsk2] that arrive in the
+        interval <<[t1, t2)>> ... *)
+    Let tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1 t2.
+
+    (** ... and let [trigger_jobs] denote the corresponding type-one jobs. *)
+    Let trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals].
+
+    (** First, note that the arrival times of the jobs in [trigger_jobs]
+        necessarily fall into the window <<[t1 - delay_bound tsk2, t2)>>. *)
+    Lemma trigger_job_arrival_bounded :
+      forall j1,
+        j1 \in trigger_jobs ->
+        (t1 - delay_bound tsk2) <= job_arrival j1 < t2.
+    Proof.
+      move: H_arr_seq_mapping => [_ _ BOUND DEF].
+      move=> j1 /mapP [j2] /[!mem_filter] /andP [SRC2 ARR2] EQ.
+      move: SRC2; rewrite /job_of_task => /eqP SRC2.
+      have /andP[j2t1 j2t2]:  t1 <= job_arrival j2 < t2.
+      { apply: job_arrival_between; last exact: ARR2.
+        exact: consistent_propagated_arrival_sequence. }
+      have BARR2: job_arrival j2 = job_arrival j1 + arrival_delay j2
+        by rewrite EQ; apply: DEF.
+      suff: arrival_delay j2 <= delay_bound tsk2; first by lia.
+      rewrite -SRC2; apply: BOUND.
+      - by rewrite SRC2.
+      - exact/arrives_in_propagated_only_if/in_arrivals_implies_arrived.
+    Qed.
+
+    (** Let [tsk1] denote the associated type-one task of [tsk1]... *)
+    Let tsk1 := task1_of tsk2.
+
+    (** ... and let [tsk1_arrivals] denote its jobs in the window during which
+        triggering jobs may arrive. *)
+    Let tsk1_arrivals := task_arrivals_between arr_seq1 tsk1 (t1 - delay_bound tsk2) t2.
+
+    (** The triggering jobs are hence a subset of all of [tsk1]'s arrivals. *)
+    Lemma subset_trigger_jobs :
+      {subset trigger_jobs <= tsk1_arrivals}.
+    Proof.
+      move=> j1 IN.
+      move: (IN) => /mapP [j2 /[!mem_filter]/andP[] TSK2 SRC2 MAP].
+      apply/andP; split.
+      { move: H_valid_mapping => [CONS _].
+        move: TSK2; rewrite /tsk1 /job_of_task MAP => /eqP <-.
+        by apply/eqP/CONS. }
+      { have /andP[Hge Hlt] := trigger_job_arrival_bounded j1 IN.
+        apply : job_in_arrivals_between => // /[!MAP].
+        exact/arrives_in_propagated_only_if/in_arrivals_implies_arrived. }
+    Qed.
+
+    (** Additionally, from the assumption that each type-one job has at most one
+        type-two successor ([H_job2_of_singleton]), we have that [job1_of] is
+        injective (for the jobs in the arrival sequence).  *)
+    Lemma job1_of_inj : {in tsk2_arrivals &, injective [eta job1_of]}.
+    Proof.
+      move=> j2 j2' IN2 IN2' EQ.
+      move: H_valid_mapping => [CONS _].
+      move: H_arr_seq_mapping => [CONS' _ _ _].
+      have SIZE: size (job2_of (job1_of j2')) <= 1.
+      { apply: (H_job2_of_singleton (task1_of (job_task j2'))).
+        - rewrite /ts1 map_f //.
+          by move: IN2'; rewrite mem_filter /job_of_task => /andP [/eqP-> _].
+        - exact: CONS. }
+      have: j2' \in job2_of (job1_of j2') by rewrite CONS'.
+      move: SIZE (EQ); rewrite -CONS'.
+      case: (job2_of _) => [//|j2'' tail].
+      case: tail => // _.
+      by rewrite !mem_seq1 => /eqP-> /eqP->.
+    Qed.
+
+    (** Finally, the sequence of triggering jobs contains no duplicates since it
+        is part of the valid arrival sequence [arr_seq1]. *)
+    Lemma uniq_trigger_jobs : uniq trigger_jobs.
+    Proof.
+      rewrite map_inj_in_uniq; last exact: job1_of_inj.
+      rewrite filter_uniq //.
+      apply: arrivals_uniq.
+      - exact: consistent_propagated_arrival_sequence.
+      - exact: propagated_arrival_sequence_uniq.
+    Qed.
+
+    (** Taken together, the above facts allow us to conclude that the magnitude
+        of [trigger_jobs] is upper-bounded by the total number of jobs released
+        by [tsk1] during <<[t1 - delay_bound tsk2, t2]>>, i.e., the count of
+        jobs in [tsk1_arrivals]. *)
+    Corollary trigger_job_size : size trigger_jobs <= size tsk1_arrivals.
+    Proof.
+      apply: uniq_leq_size.
+      - exact: uniq_trigger_jobs.
+      - exact: subset_trigger_jobs.
+    Qed.
+
+  End ArrivalCurveCorrectnessSteps.
+
+
+  (** Assuming that the given arrival sequence for type-one tasks correctly
+      bounds the arrivals of triggering jobs, [trigger_job_size] implies that
+      the derived arrival curve correctly bounds the arrivals of type-two job
+      since [size tsk1_arrivals] is then bounded by the given arrival curve
+      [max_arrivals1]. *)
+  Theorem propagated_arrival_curve_respected :
+    taskset_respects_max_arrivals arr_seq1 ts1 ->
+    taskset_respects_max_arrivals arr_seq2 ts2.
+  Proof.
+    move=> RESP1 tsk2 IN2 t1 t2 LEQ.
+    have IN1 : task1_of tsk2 \in ts1 by rewrite /ts1 map_f.
+    rewrite /max_arrivals/max_arrivals2/propagated_arrival_curve
+              /number_of_task_arrivals/task_arrivals_between.
+    case DELTA: (t2 - t1) => [|D];
+      first by rewrite arrivals_between_geq //=; lia.
+    rewrite -DELTA => {D} {DELTA}.
+    rewrite -(size_map job1_of) //.
+    apply: leq_trans; first exact: trigger_job_size.
+    apply (@leq_trans (max_arrivals (task1_of tsk2)
+                         (t2 - (t1 - delay_bound tsk2)))).
+    - rewrite -/(number_of_task_arrivals _ _ (t1 - delay_bound tsk2) t2).
+      by apply: (RESP1 _ IN1); lia.
+    - move: (H_valid_ac _ IN1) => [_ MONO].
+      by apply: MONO; lia.
+  Qed.
+
+End ACPropFacts.
+

analysis/facts/edf_definitions.v

+Require Export prosa.analysis.facts.model.ideal.schedule.
+Require Export prosa.analysis.facts.behavior.deadlines.
+Require Export prosa.analysis.definitions.schedulability.
+Require Export prosa.model.priority.edf.
+Require Export prosa.model.schedule.edf.
+Require Export prosa.model.schedule.priority_driven.
+Require Import prosa.model.readiness.basic.
+Require Import prosa.model.preemption.fully_preemptive.
+
+(** * Equivalence of EDF Definitions *)
+
+(** Recall that we have defined "EDF schedules" in two ways.
+
+    The generic way to define an EDF schedule is by using the EDF priority
+    policy defined in [model.priority.edf] and the general notion of
+    priority-compliant schedules defined in [model.schedule.priority_driven].
+
+    Another, more straight-forward way to define an EDF schedule is the standalone
+    definition given in [model.schedule.edf], which is less general but simpler
+    and used in the EDF optimality proof.
+
+    In this file, we show that both definitions are equivalent assuming:
+
+    (1) ideal uniprocessor schedules,
+
+    (2) the classic Liu & Layland model of readiness without jitter and
+    without self-suspensions, where pending jobs are always ready, and
+
+    (3) that jobs are fully preemptive. *)
+
+Section Equivalence.
+
+  (** We assume the basic (i.e., Liu & Layland)
+      readiness model under which any pending job is ready. *)
+  #[local] Existing Instance basic_ready_instance.
+
+  (** We assume that jobs are fully preemptive. *)
+  #[local] Existing Instance fully_preemptive_job_model.
+
+  (** For any given type of jobs, each characterized by an arrival time,
+      an execution cost, and an absolute deadline, ... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+  (** ...consider a given valid job arrival sequence ... *)
+  Variable arr_seq: arrival_sequence Job.
+  Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+
+  (** ...and a corresponding ideal uniprocessor schedule. *)
+  Variable sched : schedule (ideal.processor_state Job).
+
+  (** Suppose jobs don't execute before their arrival nor after their
+      completion, ... *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
+
+  (** ...all jobs come from the arrival sequence [arr_seq], ...*)
+  Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ...and jobs from [arr_seq] don't miss their deadlines. *)
+  Hypothesis H_no_deadline_misses: all_deadlines_of_arrivals_met arr_seq sched.
+
+  (** We first show that a schedule that satisfies the standalone
+      [EDF_schedule] predicate is also compliant with the generic notion of EDF
+      policy defined in Prosa, namely the [respects_policy_at_preemption_point]
+      predicate. *)
+  Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
+    EDF_schedule sched ->
+    respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
+  Proof.
+    move=> EDF j' j t ARR PREEMPTION BL SCHED.
+    have suff: exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t'.
+    { move=> [t' [/andP [LE _] SCHED']].
+      apply: (EDF t); [by [] | exact: LE | exact: SCHED' |].
+      by apply: (backlogged_implies_arrived sched j' t). }
+    apply; apply: incomplete_implies_scheduled_later.
+    - exact: H_no_deadline_misses.
+    - exact: (backlogged_implies_incomplete sched j' t).
+  Qed.
+
+  (** Conversely, the reverse direction also holds: a schedule that satisfies
+      the [respects_policy_at_preemption_point] predicate is also an EDF
+      schedule in the sense of [EDF_schedule]. *)
+  Lemma respects_policy_at_preemption_point_implies_EDF_schedule :
+    respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job) ->
+    EDF_schedule sched.
+  Proof.
+    move=> H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.
+    case (boolP (j == j_hp)); first by move /eqP => EQ; subst.
+    move /neqP => NEQ.
+    exploit (H_priority_driven j j_hp t) => //.
+    { by rewrite /preemption_time scheduled_job_at_def //; destruct (sched t). }
+    { apply /andP; split => //.
+      - apply /andP; split => //.
+        apply (incompletion_monotonic _ j _ _ LEQ).
+        by apply scheduled_implies_not_completed.
+      - apply /negP; move => SCHED''.
+        by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). }
+  Qed.
+
+  (** From the two preceding lemmas, it follows immediately that the two EDF
+      definitions are indeed equivalent, which we note with the following
+      corollary. *)
+  Corollary EDF_schedule_equiv:
+    EDF_schedule sched <-> respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
+  Proof.
+    split.
+    - exact: EDF_schedule_implies_respects_policy_at_preemption_point.
+    - exact: respects_policy_at_preemption_point_implies_EDF_schedule.
+  Qed.
+
+End Equivalence.

analysis/facts/hyperperiod.v

+Require Export prosa.analysis.definitions.hyperperiod.
+Require Export prosa.analysis.facts.periodic.task_arrivals_size.
+Require Export prosa.util.div_mod.
+Require Export prosa.util.tactics.
+
+(** In this file we prove some simple properties of hyperperiods of periodic tasks. *)
+Section Hyperperiod.
+
+  (** Consider any type of periodic tasks, ... *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** ... any task set [ts], ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... and any task [tsk] that belongs to this task set. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts: tsk \in ts.
+
+  (** A task set's hyperperiod is an integral multiple
+      of each task's period in the task set. **)
+  Lemma hyperperiod_int_mult_of_any_task:
+    exists (k : nat),
+      hyperperiod ts = k * task_period tsk.
+  Proof. by apply/dvdnP; apply lcm_seq_is_mult_of_all_ints, map_f, H_tsk_in_ts. Qed.
+
+End Hyperperiod.
+
+(** In this section we show a property of hyperperiod in context
+   of task sets with valid periods. *)
+Section ValidPeriodsImplyPositiveHP.
+
+  (** Consider any type of periodic tasks ... *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** ... and any task set [ts] ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... such that all tasks in [ts] have valid periods. *)
+  Hypothesis H_valid_periods: valid_periods ts.
+
+  (** We show that the hyperperiod of task set [ts]
+   is positive. *)
+  Lemma valid_periods_imply_pos_hp:
+    hyperperiod ts > 0.
+  Proof.
+    apply all_pos_implies_lcml_pos.
+    move => b /mapP [x IN EQ]; subst b.
+    now apply H_valid_periods.
+  Qed.
+
+End ValidPeriodsImplyPositiveHP.
+
+(** In this section we prove some lemmas about the hyperperiod
+    in context of the periodic model. *)
+Section PeriodicLemmas.
+
+  (** Consider any type of tasks, ... *)
+  Context {Task : TaskType}.
+  Context `{TaskOffset Task}.
+  Context `{PeriodicModel Task}.
+
+  (** ... any type of jobs, ... *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+
+  (** ... and a consistent arrival sequence with non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** Consider a task set [ts] such that all tasks in
+      [ts] have valid periods. *)
+  Variable ts : TaskSet Task.
+  Hypothesis H_valid_periods: valid_periods ts.
+
+  (** Let [tsk] be any periodic task in [ts] with a valid offset and period. *)
+  Variable tsk : Task.
+  Hypothesis H_task_in_ts: tsk \in ts.
+  Hypothesis H_valid_offset: valid_offset arr_seq tsk.
+  Hypothesis H_valid_period: valid_period tsk.
+  Hypothesis H_periodic_task: respects_periodic_task_model arr_seq tsk.
+
+  (** Assume we have an infinite sequence of jobs in the arrival sequence. *)
+  Hypothesis H_infinite_jobs: infinite_jobs arr_seq.
+
+  (** Let [O_max] denote the maximum task offset in [ts] and let
+   [HP] denote the hyperperiod of all tasks in [ts]. *)
+  Let O_max := max_task_offset ts.
+  Let HP := hyperperiod ts.
+
+  (** We show that the job corresponding to any job [j1] in any other
+      hyperperiod is of the same task as [j1]. *)
+  Lemma corresponding_jobs_have_same_task:
+    forall j1 j2,
+      job_task (corresponding_job_in_hyperperiod ts arr_seq j1
+               (starting_instant_of_corresponding_hyperperiod ts j2) (job_task j1)) = job_task j1.
+  Proof.
+    clear H_task_in_ts H_valid_period.
+    move=> j1 j2.
+    set ARRIVALS := (task_arrivals_between arr_seq (job_task j1) (starting_instant_of_hyperperiod ts (job_arrival j2))
+          (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)).
+    set IND := (job_index_in_hyperperiod ts arr_seq j1 (starting_instant_of_hyperperiod ts (job_arrival j1)) (job_task j1)).
+    have SIZE_G : size ARRIVALS <= IND -> job_task (nth j1 ARRIVALS IND) = job_task j1 by intro SG; rewrite nth_default.
+    case: (boolP (size ARRIVALS == IND)) => [/eqP EQ|NEQ]; first by apply SIZE_G; lia.
+    move : NEQ; rewrite neq_ltn; move => /orP [LT | G]; first by apply SIZE_G; lia.
+    set jb := nth j1 ARRIVALS IND.
+    have JOB_IN : jb \in ARRIVALS by apply mem_nth.
+    rewrite /ARRIVALS /task_arrivals_between mem_filter in JOB_IN.
+    now move : JOB_IN => /andP [/eqP TSK JB_IN].
+  Qed.
+
+  (** We show that if a job [j] lies in the hyperperiod starting
+   at instant [t] then [j] arrives in the interval <<[t, t + HP)>>. *)
+  Lemma all_jobs_arrive_within_hyperperiod:
+    forall j t,
+      j \in jobs_in_hyperperiod ts arr_seq t tsk->
+      t <= job_arrival j < t + HP.
+  Proof.
+    intros * JB_IN_HP.
+    rewrite mem_filter in JB_IN_HP.
+    move : JB_IN_HP => /andP [/eqP TSK JB_IN]; apply mem_bigcat_nat_exists in JB_IN.
+    destruct JB_IN as [i [JB_IN INEQ]].
+    apply job_arrival_at in JB_IN => //.
+    by rewrite JB_IN.
+  Qed.
+
+  (** We show that the number of jobs in a hyperperiod starting at [n1 * HP + O_max]
+   is the same as the number of jobs in a hyperperiod starting at [n2 * HP + O_max] given
+   that [n1] is less than or equal to [n2]. *)
+  Lemma eq_size_hyp_lt:
+    forall n1 n2,
+      n1 <= n2 ->
+      size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
+      size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk).
+  Proof.
+    move=> n1 n2 N1_LT.
+    have -> : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP.
+    { by rewrite -[in LHS](subnKC N1_LT) mulnDl addnAC. }
+    destruct (hyperperiod_int_mult_of_any_task ts tsk H_task_in_ts) as [k HYP]; rewrite !/HP.
+    rewrite [in X in _ = size (_ (n1 * HP + O_max + _ * X) tsk)]HYP.
+    rewrite mulnA /HP /jobs_in_hyperperiod !size_of_task_arrivals_between.
+    erewrite big_sum_eq_in_eq_sized_intervals => //; intros g G_LT.
+    have OFF_G : task_offset tsk <= O_max by apply max_offset_g.
+    have FG : forall v b n, v + b + n = v + n + b by intros *; lia.
+    erewrite eq_size_of_task_arrivals_seperated_by_period => //; last lia.
+    by rewrite FG.
+  Qed.
+
+  (** We generalize the above lemma by lifting the condition on
+   [n1] and [n2]. *)
+  Lemma eq_size_of_arrivals_in_hyperperiod:
+    forall n1 n2,
+      size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
+      size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk).
+  Proof.
+    move=> n1 n2.
+    case : (boolP (n1 == n2)) => [/eqP EQ | NEQ]; first by rewrite EQ.
+    move : NEQ; rewrite neq_ltn; move => /orP [LT | LT].
+    + by apply eq_size_hyp_lt => //; lia.
+    + move : (eq_size_hyp_lt n2 n1) => EQ_S.
+      by feed_n 1 EQ_S => //; lia.
+  Qed.
+
+  (** Consider any two jobs [j1] and [j2] that stem from the arrival sequence
+   [arr_seq] such that [j1] is of task [tsk]. *)
+  Variable j1 : Job.
+  Variable j2 : Job.
+  Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
+  Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
+  Hypothesis H_j1_task: job_task j1 = tsk.
+
+  (** Assume that both [j1] and [j2] arrive after [O_max]. *)
+  Hypothesis H_j1_arr_after_O_max: O_max <= job_arrival j1.
+  Hypothesis H_j2_arr_after_O_max: O_max <= job_arrival j2.
+
+  (** We show that any job [j] that arrives in task arrivals in the same
+      hyperperiod as [j2] also arrives in task arrivals up to [job_arrival j2 + HP]. *)
+  Lemma job_in_hp_arrives_in_task_arrivals_up_to:
+    forall j,
+      j \in jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk ->
+      j \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
+  Proof.
+    intros j J_IN.
+    rewrite /task_arrivals_up_to.
+    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk).
+    move : (J_IN) => J_ARR; apply all_jobs_arrive_within_hyperperiod in J_IN.
+    rewrite /jobs_in_hp /jobs_in_hyperperiod /task_arrivals_up_to /task_arrivals_between mem_filter in J_ARR.
+    move : J_ARR =>  /andP [/eqP TSK' NTH_IN].
+    apply job_in_task_arrivals_between => //;
+      first by apply in_arrivals_implies_arrived in NTH_IN.
+    apply mem_bigcat_nat_exists in NTH_IN.
+    apply /andP; split => //.
+    rewrite ltnS.
+    apply leq_trans with (n := (job_arrival j2 - O_max) %/ HP * HP + O_max + HP); first by lia.
+    rewrite leq_add2r.
+    have O_M : (job_arrival j2 - O_max) %/ HP * HP <= job_arrival j2 - O_max by apply leq_trunc_div.
+    have ARR_G : job_arrival j2 >= O_max by [].
+    lia.
+  Qed.
+
+  (** We show that job [j1] arrives in its own hyperperiod. *)
+  Lemma job_in_own_hp:
+    j1 \in jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk.
+  Proof.
+    apply job_in_task_arrivals_between => //.
+    apply /andP; split.
+    + rewrite addnC -leq_subRL => //.
+      by apply leq_trunc_div.
+    + specialize (div_floor_add_g (job_arrival j1 - O_max) HP) => AB.
+      feed_n 1 AB; first by apply valid_periods_imply_pos_hp => //.
+      rewrite ltn_subLR // in AB.
+      by rewrite -/(HP); lia.
+  Qed.
+
+  (** We show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod
+   arrives in task arrivals up to [job_arrival j2 + HP]. *)
+  Lemma corr_job_in_task_arrivals_up_to:
+    corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk \in
+      task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
+  Proof.
+    rewrite /corresponding_job_in_hyperperiod /starting_instant_of_corresponding_hyperperiod.
+    rewrite /job_index_in_hyperperiod /starting_instant_of_hyperperiod /hyperperiod_index.
+    set ind := (index j1 (jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk)).
+    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk).
+    set nj := nth j1 jobs_in_hp ind.
+    apply job_in_hp_arrives_in_task_arrivals_up_to => //.
+    rewrite mem_nth /jobs_in_hp => //.
+    specialize (eq_size_of_arrivals_in_hyperperiod ((job_arrival j2 - O_max) %/ HP) ((job_arrival j1 - O_max) %/ HP)) => EQ.
+    rewrite EQ /ind index_mem.
+    by apply job_in_own_hp.
+  Qed.
+
+  (** Finally, we show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod
+   arrives in the arrival sequence [arr_seq]. *)
+  Lemma corresponding_job_arrives:
+      arrives_in arr_seq (corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk).
+  Proof.
+    move : (corr_job_in_task_arrivals_up_to) => ARR_G.
+    rewrite /task_arrivals_up_to /task_arrivals_between mem_filter in ARR_G.
+    move : ARR_G =>  /andP [/eqP TSK' NTH_IN].
+    by apply in_arrivals_implies_arrived in NTH_IN.
+  Qed.
+
+End PeriodicLemmas.

analysis/facts/interference.v

+Require Export prosa.analysis.facts.priority.classes.
+Require Export prosa.analysis.definitions.interference.
+Require Export prosa.analysis.definitions.priority.classes.
+Require Export prosa.analysis.facts.model.service_of_jobs.
+
+(** * Auxiliary Lemmas about Interference *)
+
+(** If there is a priority policy in the context, one can
+    differentiate between interference (interfering workload) that
+    comes from jobs with higher or lower priority from other sources
+    of interference (interfering workload).
+
+    Unfortunately, instantiated functions usually do not come with any
+    useful lemmas about them. In order to reuse existing lemmas, we
+    need to prove equivalence of the instantiated functions to some
+    conventional notions. *)
+
+(** First, we prove several lemmas about interference in the context
+    of priority policies involving both FP and JLFP relations. *)
+Section InterferenceProperties.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType} {jt : JobTask Job Task}.
+
+  (** Consider any kind of processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** Consider a reflexive FP-policy and a JLFP policy compatible with it. *)
+  Context {FP : FP_policy Task} {JLFP : JLFP_policy Job}.
+  Hypothesis H_compatible : JLFP_FP_compatible JLFP FP.
+  Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.
+
+  (** We observe that any higher-priority job must come from a task with
+      either higher or equal priority. *)
+  Lemma another_task_hep_job_split_hp_ep :
+    forall j1 j2,
+      another_task_hep_job j1 j2
+      = hp_task_hep_job j1 j2 || other_ep_task_hep_job j1 j2.
+  Proof.
+    move=> j1 j2; rewrite -[X in _ || X]andbA -andb_orr /another_task_hep_job.
+    have [hepj1j2/=|//] := boolP (hep_job j1 j2).
+    rewrite -[hp_task _ _](@andb_idr _ (job_task j1 != job_task j2)).
+    - by rewrite -andb_orl -hep_hp_ep_task hep_job_implies_hep_task.
+    - by apply: contraTN => /eqP->; rewrite hp_task_irrefl.
+  Qed.
+
+  (** We establish a higher-or-equal job of another task causing interference,
+      can be due to a higher priority task or an equal priority task. *)
+  Lemma hep_interference_another_task_split :
+    forall j t,
+      another_task_hep_job_interference arr_seq sched j t
+      = hep_job_from_hp_task_interference arr_seq sched j t
+        || hep_job_from_other_ep_task_interference arr_seq sched j t.
+  Proof.
+    move => j t; rewrite -has_predU; apply: eq_in_has => j' _ /=.
+    exact: another_task_hep_job_split_hp_ep.
+  Qed.
+
+  (** Now, assuming a uniprocessor model,... *)
+  Hypothesis H_uniproc : uniprocessor_model PState.
+
+  (** ...the previous lemma allows us to establish that the cumulative interference incurred by a job
+      is equal to the sum of the cumulative interference from higher-or-equal-priority jobs belonging to
+      strictly higher-priority tasks (FP) and the cumulative interference from higher-or-equal-priority
+      jobs belonging to equal-priority tasks (GEL). *)
+  Lemma cumulative_hep_interference_split_tasks_new :
+    forall j t1 Δ,
+    cumulative_another_task_hep_job_interference arr_seq  sched j t1 (t1 + Δ)
+    = cumulative_interference_from_hep_jobs_from_hp_tasks arr_seq sched j t1 (t1 + Δ)
+      + cumulative_interference_from_hep_jobs_from_other_ep_tasks arr_seq sched j t1 (t1 + Δ).
+  Proof.
+    move => j t1 Δ.
+    rewrite -big_split //=; apply: eq_big_seq => t IN.
+    rewrite hep_interference_another_task_split.
+    have: forall a b, ~~ (a && b) -> (a || b) = a + b :> nat by case; case.
+    apply; apply/negP => /andP[/hasP[j' + hp] /hasP[j'' + ep]].
+    rewrite !mem_filter => /andP[sj' _] /andP[sj'' _].
+    move: hp ep; have ->: j'' = j' by exact: only_one_job_receives_service_at_uni.
+    move=> /andP[_ /andP[_ +]] /andP[/andP[_ +] _].
+    by rewrite hep_hp_ep_task negb_or ep_task_sym => /andP[_ /negbTE].
+  Qed.
+
+End InterferenceProperties.
+
+(** In the following section, we prove a few properties of
+    interference under a JLFP policy. *)
+Section InterferencePropertiesJLFP.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of fully supply-consuming uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any valid arrival sequence with consistent arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any uni-processor schedule of this arrival
+      sequence ... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence :
+    jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival or after
+      completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Let [tsk] be any task. *)
+  Variable tsk : Task.
+
+  (** In the following, consider a JLFP-policy that indicates a
+      higher-or-equal priority relation, and assume that this relation
+      is reflexive and transitive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
+
+  (** First, we prove a few rewriting rules under the assumption that
+      there is no supply. *)
+  Section NoSupply.
+
+    (** Consider a time instant [t] ... *)
+    Variable t : instant.
+
+    (** ... and assume that there is no supply at [t]. *)
+    Hypothesis H_no_supply : ~~ has_supply sched t.
+
+    (** Then, there is no interference from higher-or-equal priority
+        jobs ... *)
+    Lemma no_hep_job_interference_without_supply :
+      forall j, ~~ another_hep_job_interference arr_seq sched j t.
+    Proof.
+      move=> j; apply/hasPn => [s IN]; exfalso.
+      move: IN; rewrite mem_filter => /andP [SERV _].
+      move: (H_no_supply) => /negP NSUP; apply: NSUP.
+      by apply: receives_service_implies_has_supply.
+    Qed.
+
+    (** ... and that there is no interference from higher-or-equal
+        priority jobs from other tasks. *)
+    Lemma no_hep_task_interference_without_supply :
+      forall j, ~~ another_task_hep_job_interference arr_seq sched j t.
+    Proof.
+      move=> j; apply/hasPn => [s IN]; exfalso.
+      move: IN; rewrite mem_filter => /andP [SERV _].
+      move: (H_no_supply) => /negP NSUP; apply: NSUP.
+      by apply: receives_service_implies_has_supply.
+    Qed.
+
+  End NoSupply.
+
+  (** In the following subsection, we prove properties of the
+      introduced functions under the assumption that the schedule is
+      idle. *)
+  Section Idle.
+
+    (** Consider a time instant [t] ... *)
+    Variable t : instant.
+
+    (** ... and assume that the schedule is idle at [t]. *)
+    Hypothesis H_idle : is_idle arr_seq sched t.
+
+    (** We prove that in this case: ... *)
+
+    (** ... there is no interference from higher-or-equal priority
+        jobs ... *)
+    Lemma no_hep_job_interference_when_idle :
+      forall j, ~~ another_hep_job_interference arr_seq sched j t.
+    Proof.
+      move=> j; apply/hasPn=> jo SERV; exfalso.
+      rewrite mem_filter in SERV; move: SERV => /andP [SERV _].
+      by apply/negP; first apply: no_service_received_when_idle => //. 
+    Qed.
+
+    (** ... and that there is no interference from higher-or-equal
+        priority jobs from other tasks. *)
+    Lemma no_hep_task_interference_when_idle :
+      forall j, ~~ another_task_hep_job_interference arr_seq sched j t.
+    Proof.
+      move=> j; apply/hasPn=> jo SERV; exfalso.
+      rewrite mem_filter in SERV; move: SERV => /andP [SERV _].
+      by apply/negP; first apply: no_service_received_when_idle => //. 
+    Qed.
+
+  End Idle.
+
+  (** Next, we prove properties of the introduced functions under the
+      assumption that there is supply and the scheduler is not
+      idle. *)
+  Section SupplyAndScheduledJob.
+
+    (** Consider a job [j] of task [tsk]. In this subsection, job [j]
+        is deemed to be the main job with respect to which the
+        functions are computed. *)
+    Variable j : Job.
+    Hypothesis H_j_tsk : job_of_task tsk j.
+
+    (** Consider a time instant [t] ... *)
+    Variable t : instant.
+
+    (** ... and assume that there is supply at [t]. *)
+    Hypothesis H_supply : has_supply sched t.
+
+    (** First, consider a case when _some_ job is scheduled at time [t]. *)
+    Section SomeJobIsScheduled.
+
+      (** Consider a job [j'] (not necessarily distinct from job [j])
+          that is scheduled at time [t]. *)
+      Variable j' : Job.
+      Hypothesis H_sched : scheduled_at sched j' t.
+
+      (** Under the stated assumptions, we show that the interference
+          from another higher-or-equal priority job is equivalent to
+          the relation [another_hep_job]. *)
+      Lemma interference_ahep_def :
+        another_hep_job_interference arr_seq sched j t = another_hep_job j' j.
+      Proof.
+        clear H_j_tsk.
+        apply/idP/idP => [/hasP[jhp /[!mem_filter]/andP[PSERV IN] AHEP] | AHEP].
+        { apply service_at_implies_scheduled_at in PSERV.
+          have EQ: jhp = j' by apply: H_uniprocessor_proc_model.
+          by subst j'. }
+        { apply/hasP; exists j' => //.
+          by apply receives_service_and_served_at_consistent, ideal_progress_inside_supplies. }
+      Qed.
+
+      (** Similarly, we show that the interference from another
+          higher-or-equal priority job from another task is equivalent
+          to the relation [another_task_hep_job]. *)
+      Lemma interference_athep_def :
+        another_task_hep_job_interference arr_seq sched j t = another_task_hep_job j' j.
+      Proof.
+        apply/idP/idP => [/hasP[jhp /[!mem_filter]/andP[PSERV IN] AHEP] | AHEP].
+        - apply service_at_implies_scheduled_at in PSERV.
+          have EQ: jhp = j' by apply: H_uniprocessor_proc_model.
+          by subst.
+        - apply/hasP; exists j' => //; rewrite mem_filter; apply/andP; split.
+          + by apply: progress_inside_supplies => //.
+          + by apply: arrivals_up_to_scheduled_at.
+      Qed.
+
+    End SomeJobIsScheduled.
+
+    (** Next, consider a case when [j] itself is scheduled at [t]. *)
+    Section JIsScheduled.
+
+      (** Assume that [j] is scheduled at time [t]. *)
+      Hypothesis H_j_sched : scheduled_at sched j t.
+
+      (** Then there is no interference from higher-or-equal priority
+          jobs at time [t]. *)
+      Lemma no_ahep_interference_when_scheduled :
+        ~~ another_hep_job_interference arr_seq sched j t.
+      Proof.
+        apply/negP; move=> /hasP[jhp /[!mem_filter]/andP[PSERV IN] AHEP].
+        apply service_at_implies_scheduled_at in PSERV.
+        have EQ: jhp = j; [by apply: H_uniprocessor_proc_model | subst jhp].
+        by apply another_hep_job_antireflexive in AHEP.
+      Qed.
+
+    End JIsScheduled.
+
+    (** Next, consider a case when [j] receives service at [t]. *)
+    Section JIsServed.
+
+      (** Assume that [j] receives service at time [t]. *)
+      Hypothesis H_j_served : receives_service_at sched j t.
+
+      (** Then there is no interference from higher-or-equal priority
+          jobs at time [t]. *)
+      Lemma no_ahep_interference_when_served :
+        ~~ another_hep_job_interference arr_seq sched j t.
+      Proof.
+        apply/negP => INT.
+        rewrite (interference_ahep_def j) in INT => //; first last.
+        - by apply service_at_implies_scheduled_at.
+        - by move: INT => /andP [_ ]; rewrite eq_refl.
+      Qed.
+
+    End JIsServed.
+
+    (** In the next subsection, we consider a case when a job [j']
+        from the same task (as job [j]) is scheduled. *)
+    Section FromSameTask.
+
+      (** Consider a job [j'] that comes from task [tsk] and is
+          scheduled at time instant [t].  *)
+      Variable j' : Job.
+      Hypothesis H_j'_tsk : job_of_task tsk j'.
+      Hypothesis H_j'_sched : scheduled_at sched j' t.
+
+      (** Then we show that there is no interference from
+          higher-or-equal priority jobs of another task. *)
+      Lemma no_athep_interference_when_scheduled :
+        ~~ another_task_hep_job_interference arr_seq sched j t.
+      Proof.
+        apply/negP; move=> /hasP[jhp /[!mem_filter]/andP[PSERV IN] AHEP].
+        apply service_at_implies_scheduled_at in PSERV.
+        have EQ: jhp = j'; [by apply: H_uniprocessor_proc_model | subst jhp].
+        by eapply another_task_hep_job_taskwise_antireflexive in AHEP.
+      Qed.
+
+    End FromSameTask.
+
+    (** In the next subsection, we consider a case when a job [j']
+        from a task other than [j]'s task is scheduled. *)
+    Section FromDifferentTask.
+
+      (** Consider a job [j'] that _does_ _not_ comes from task
+            [tsk] and is scheduled at time instant [t].  *)
+      Variable j' : Job.
+      Hypothesis H_j'_not_tsk : ~~ job_of_task tsk j'.
+      Hypothesis H_j'_sched : scheduled_at sched j' t.
+
+      (** We prove that then [j] incurs higher-or-equal priority
+          interference from another task iff [j'] has higher-or-equal
+          priority than [j]. *)
+      Lemma athep_interference_iff :
+        another_task_hep_job_interference arr_seq sched j t = hep_job j' j.
+      Proof.
+        apply/idP/idP => [/hasP[j'' /[!mem_filter]/andP[RSERV IN] AHEP] | HEP].
+        - apply service_at_implies_scheduled_at in RSERV.
+          have EQ: j' = j''; [by apply: H_uniprocessor_proc_model | subst j''].
+          by move: AHEP => /andP[].
+        - apply/hasP; exists j'; [rewrite !mem_filter|]; apply/andP; split => //.
+          + by apply ideal_progress_inside_supplies => //.
+          + apply: arrived_between_implies_in_arrivals => //.
+            apply/andP; split=> [//|].
+            by apply H_jobs_must_arrive_to_execute in H_j'_sched; rewrite ltnS.
+          + by apply: contraNN H_j'_not_tsk => /eqP; rewrite /job_of_task => ->.
+      Qed.
+
+      (** Hence, if we assume that [j'] has higher-or-equal priority, ... *)
+      Hypothesis H_j'_hep : hep_job j' j.
+
+      (** ... we are able to show that [j] incurs higher-or-equal
+          priority interference from another task. *)
+      Lemma athep_interference_if :
+        another_task_hep_job_interference arr_seq sched j t.
+      Proof.
+        by rewrite athep_interference_iff.
+      Qed.
+
+    End FromDifferentTask.
+
+    (** In the last subsection, we consider a case when the scheduled
+        job [j'] has lower priority than job [j]. *)
+    Section LowerPriority.
+
+      (** Consider a job [j'] that has lower priority than job [j]
+            and is scheduled at time instant [t].  *)
+      Variable j' : Job.
+      Hypothesis H_j'_sched : scheduled_at sched j' t.
+      Hypothesis H_j'_lp : ~~ hep_job j' j.
+
+      (** We prove that, in this case, there is no interference from
+          higher-or-equal priority jobs at time [t]. *)
+      Lemma no_ahep_interference_when_scheduled_lp :
+        ~~ another_hep_job_interference arr_seq sched j t.
+      Proof.
+        apply/negP; move/hasP => [jlp /[!mem_filter]/andP[+ IN] AHEP].
+        move/service_at_implies_scheduled_at => RSERV.
+        have EQ: j' = jlp; [by apply: H_uniprocessor_proc_model | subst j'].
+        by move: (H_j'_lp) AHEP => LP /andP [HEP A]; rewrite HEP in LP.
+      Qed.
+
+    End LowerPriority.
+
+  End SupplyAndScheduledJob.
+
+  (** In this section, we prove that the (abstract) cumulative
+      interference of jobs with higher or equal priority is equal to
+      total service of jobs with higher or equal priority. *)
+  Section InstantiatedServiceEquivalences.
+
+    (** First, let us assume that the introduced processor model is
+          unit-service. *)
+    Hypothesis H_unit_service : unit_service_proc_model PState.
+
+    (** Consider any job [j] of [tsk]. *)
+    Variable j : Job.
+    Hypothesis H_j_arrives : arrives_in arr_seq j.
+    Hypothesis H_job_of_tsk : job_of_task tsk j.
+
+    (** We consider an arbitrary time interval <<[t1, t)>> that starts
+        with a (classic) quiet time. *)
+    Variable t1 t : instant.
+    Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.
+
+    (** As follows from lemma [cumulative_pred_served_eq_service], the
+        (abstract) instantiated function of interference is equal to
+        the total service of any subset of jobs with higher or equal
+        priority. *)
+
+    (** The above is in particular true for the jobs other than [j]
+        with higher or equal priority... *)
+    Lemma  cumulative_i_ohep_eq_service_of_ohep :
+      cumulative_another_hep_job_interference arr_seq sched j t1 t
+      = service_of_other_hep_jobs arr_seq sched j t1 t.
+    Proof.
+      apply: cumulative_pred_served_eq_service => //.
+      - by move => ? /andP[].
+    Qed.
+
+    (** ...and for jobs from other tasks than [j] with higher
+        or equal priority. *)
+    Lemma cumulative_i_thep_eq_service_of_othep :
+      cumulative_another_task_hep_job_interference arr_seq sched j t1 t
+      = service_of_other_task_hep_jobs arr_seq sched j t1 t.
+    Proof.
+      apply: cumulative_pred_served_eq_service => //.
+      by move => ? /andP[].
+    Qed.
+
+  End InstantiatedServiceEquivalences.
+
+End InterferencePropertiesJLFP.

analysis/facts/jitter.v

+Require Export prosa.analysis.facts.delay_propagation.
+Require Export prosa.model.schedule.work_conserving.
+Require Export prosa.model.readiness.basic.
+Require Export prosa.model.schedule.priority_driven.
+Require Export prosa.analysis.definitions.schedulability.
+
+(** * Propagation of Release Jitter in Arrival Curves *)
+
+(** In this module, we prove correct an approach to "hiding" release jitter by
+    "folding" it into arrival curves. *)
+Section JitterPropagationFacts.
+
+  (** Consider any type of tasks described by arrival curves and the
+      corresponding jobs. *)
+  Context {Task : TaskType} {arrival_curve : MaxArrivals Task}
+          {Job : JobType} `{JobTask Job Task}.
+
+  (** Let [original_arrival] denote each job's _actual_ arrival time ... *)
+  Context {original_arrival : JobArrival Job}.
+
+  (** ... and suppose the jobs are affected by bounded release jitter. *)
+  Context `{TaskJitter Task} `{JobJitter Job}.
+
+  (** In the following, consider an arbitrary valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** Recall the induced "release curve" and associated definitions. *)
+  #[local] Existing Instance release_as_arrival.
+  #[local] Existing Instance release_curve.
+
+  (** In the following, we let [rel_seq] denote the induced "release curve". *)
+  Let rel_seq := release_sequence arr_seq.
+
+  (** Suppose we are given a set of tasks ... *)
+  Variable ts : seq Task.
+
+  (** ... with valid bounds on release jitter. *)
+  Hypothesis H_valid_jitter : valid_jitter_bounds ts.
+
+  (** ** Restated General Properties *)
+
+  (** We begin by restating general properties of delay propagation, specialized
+      to the case of jitter propagation. *)
+
+  (** The arrival and release sequences contain an identical set of jobs. *)
+  Corollary jitter_arrives_in_iff :
+    forall j,
+      arrives_in arr_seq j <-> arrives_in rel_seq j.
+  Proof.
+    move=> j; split;
+          [ apply: (arrives_in_propagated_if original_arrival release_as_arrival) => //
+          | apply: (arrives_in_propagated_only_if original_arrival release_as_arrival) => //
+          ]; exact: jitter_arr_seq_mapping_valid.
+  Qed.
+
+  (** The induced "release sequence" is valid. *)
+  Corollary valid_release_sequence :
+    @valid_arrival_sequence _ release_as_arrival rel_seq.
+  Proof.
+    apply: (valid_propagated_arrival_sequence original_arrival release_as_arrival) => //.
+    by apply: jitter_arr_seq_mapping_valid.
+  Qed.
+
+  (** If the arrival curve is structurally valid, then so is the induced release
+      curve. *)
+  Corollary valid_release_curve :
+    valid_taskset_arrival_curve ts max_arrivals ->
+    valid_taskset_arrival_curve ts release_curve.
+  Proof.
+    move=> VALID.
+    apply: propagated_arrival_curve_valid => tsk IN.
+    by move: (VALID tsk IN) => [_ {}].
+  Qed.
+
+  (** Furthermore, if the arrival curve correctly bounds arrivals according to
+      [arr_seq], then the "release curve" also correctly bounds releases
+      according to [rel_seq]. *)
+  Corollary release_curve_respected :
+    valid_taskset_arrival_curve ts max_arrivals ->
+    @taskset_respects_max_arrivals _ _ _ arr_seq arrival_curve ts ->
+    @taskset_respects_max_arrivals _ _ _ rel_seq release_curve ts.
+  Proof.
+    move=> AC VALID.
+    apply: (propagated_arrival_curve_respected original_arrival release_as_arrival) => //; try by rewrite map_id.
+    - by apply: jitter_delay_mapping_valid.
+    - by apply: jitter_arr_seq_mapping_valid.
+  Qed.
+
+
+  (** ** Jitter Propagation Properties *)
+
+  (** Next, we establish validity properties specific to jitter
+      propagation. These are needed to apply response-time analysis results. *)
+
+  (** Since the arrival and release sequence describe identical sets of jobs,
+      trivially all jobs continue to belong to the tasks in the task set. *)
+  Lemma jitter_prop_same_jobs :
+      all_jobs_from_taskset arr_seq ts ->
+      all_jobs_from_taskset rel_seq ts.
+  Proof. by move=> ALL j IN; apply: ALL; rewrite jitter_arrives_in_iff. Qed.
+
+  (** Next, consider an arbitrary schedule of the workload. *)
+  Context {PState : ProcessorState Job}.
+  Variable sched : schedule PState.
+
+  (** Again, trivially, all jobs in the schedule continue to belong to the
+      release sequence. *)
+  Lemma jitter_prop_same_jobs' :
+      jobs_come_from_arrival_sequence sched arr_seq ->
+      jobs_come_from_arrival_sequence sched rel_seq.
+  Proof. move=> FROM j t SCHED; rewrite -jitter_arrives_in_iff; exact: FROM. Qed.
+
+  (** Let us now consider the execution costs. *)
+  Context `{JobCost Job} `{TaskCost Task}.
+
+  (** Since the set of jobs didn't change, and since release jitter propagation
+      does not change execution costs, job costs remain trivially valid. *)
+  Lemma jitter_prop_valid_costs :
+    arrivals_have_valid_job_costs arr_seq ->
+    arrivals_have_valid_job_costs rel_seq.
+  Proof.
+    move=> VALID j IN.
+    apply: VALID.
+    by rewrite jitter_arrives_in_iff.
+  Qed.
+
+  (** If the given schedule respects release jitter, then it continues to do so
+      after we've reinterpreted the release times to be the arrival times. *)
+  Lemma jitter_ready_to_execute :
+    @jobs_must_be_ready_to_execute _ _ sched _ original_arrival jitter_ready_instance ->
+    @jobs_must_be_ready_to_execute _ _ sched _ release_as_arrival basic_ready_instance.
+  Proof. move=> RDY j t SCHED; by move: (RDY j t SCHED). Qed.
+
+  (** If the schedule is work-conserving, then it continues to be so after we've
+      "hidden" release jitter by reinterpreting release times as arrival
+      times. *)
+  Theorem jitter_work_conservation :
+    @work_conserving _ original_arrival _ _ jitter_ready_instance arr_seq sched ->
+    @work_conserving _ release_as_arrival _ _ basic_ready_instance rel_seq sched.
+  Proof.
+    move=> WC_jit j t ARR_rel /andP [R_rel NSCHED].
+    have ARR_arr: arrives_in arr_seq j by rewrite jitter_arrives_in_iff.
+    apply: WC_jit; first exact: ARR_arr.
+    by apply/andP; split.
+  Qed.
+
+  (** If the given schedule is valid w.r.t. to original arrivals, then it
+      continues to be valid after reinterpreting release times as arrival
+      times. *)
+  Lemma jitter_valid_schedule :
+    @valid_schedule _ _ sched _ original_arrival jitter_ready_instance arr_seq ->
+    @valid_schedule _ _ sched _ release_as_arrival basic_ready_instance rel_seq.
+  Proof.
+    move => [SRC RDY].
+    split.
+    - exact: jitter_prop_same_jobs'.
+    - exact: jitter_ready_to_execute.
+  Qed.
+
+  (** In the following, suppose the given schedule is valid w.r.t. the original
+      arrival times and jitter-affected readiness. *)
+  Hypothesis H_valid_schedule :
+    @valid_schedule _ _ sched _ original_arrival jitter_ready_instance arr_seq.
+
+  (** As one would think, the set of scheduled jobs remains unchanged. For
+      technical reasons (dependence of the definition of [scheduled_jobs_at] on
+      the arrival sequence), this is a lot less obvious at the Coq level than
+      one intuitively might expect. *)
+  Lemma jitter_scheduled_jobs_at_equiv :
+    forall t j,
+      (j \in scheduled_jobs_at rel_seq sched t) =
+      (j \in scheduled_jobs_at arr_seq sched t).
+  Proof.
+    move=> j t.
+    have SRC := @valid_schedule_jobs_come_from_arrival_sequence _ _ sched _
+                  original_arrival jitter_ready_instance arr_seq H_valid_schedule.
+    rewrite [RHS]scheduled_jobs_at_iff; [| |exact: SRC|] => //.
+    rewrite (@scheduled_jobs_at_iff _ release_as_arrival); first by done.
+    - exact: valid_release_sequence.
+    - exact: jitter_prop_same_jobs'.
+    - exact
+        /(@jobs_must_arrive_to_be_ready _ _ sched _ release_as_arrival basic_ready_instance)
+        /jitter_ready_to_execute.
+  Qed.
+
+  (** Unsurprisingly, on a uniprocessor, the scheduled job remains unchanged,
+      too. Again, this is less straightforward than one might think due to
+      technical reasons (type-class resolution). *)
+  Lemma jitter_scheduled_job_at_eq :
+    forall t,
+      uniprocessor_model PState ->
+      scheduled_job_at arr_seq sched t = scheduled_job_at rel_seq sched t.
+  Proof.
+    move=> t UNI.
+    have SRC := @valid_schedule_jobs_come_from_arrival_sequence _ _ sched _
+                  original_arrival jitter_ready_instance arr_seq H_valid_schedule.
+    (* Note: there is a lot of repetition here because the automation chokes on
+       the multiple available type-class instances and/or promptly picks the
+       wrong ones. Not pretty, but it works. *)
+    case SCHED: scheduled_job_at => [j|];
+      case SCHED': scheduled_job_at => [j'|]; last by done.
+    { move: SCHED => /eqP; rewrite scheduled_job_at_scheduled_at; [| |exact: SRC| |] => // SCHED.
+      move: SCHED' => /eqP; rewrite (@scheduled_job_at_scheduled_at _ release_as_arrival).
+      - move=> SCHED'.
+        by rewrite (UNI j j' sched t).
+      - exact: valid_release_sequence.
+      - exact: jitter_prop_same_jobs'.
+      - exact
+          /(@jobs_must_arrive_to_be_ready _ _ sched _ release_as_arrival basic_ready_instance)
+            /jitter_ready_to_execute.
+      - by [].
+    }
+    { exfalso.
+      move: SCHED => /eqP; rewrite scheduled_job_at_scheduled_at; [| |exact: SRC| |] => //.
+      move: SCHED'; rewrite (@scheduled_job_at_none _ release_as_arrival);
+        first by move=> NSCHED; apply/negP.
+      - exact: valid_release_sequence.
+      - exact: jitter_prop_same_jobs'.
+      - exact
+          /(@jobs_must_arrive_to_be_ready _ _ sched _ release_as_arrival basic_ready_instance)
+            /jitter_ready_to_execute. }
+
+    { exfalso.
+      move: SCHED; rewrite scheduled_job_at_none; [| |exact: SRC|] => // NSCHED.
+      move: SCHED' => /eqP; rewrite (@scheduled_job_at_scheduled_at _ release_as_arrival);
+        first by apply/negP.
+      - exact: valid_release_sequence.
+      - exact: jitter_prop_same_jobs'.
+      - exact
+          /(@jobs_must_arrive_to_be_ready _ _ sched _ release_as_arrival basic_ready_instance)
+            /jitter_ready_to_execute.
+      - by []. }
+  Qed.
+
+  (** Importantly, the schedule remains FP-policy compliant if it was so to
+      begin with, despite the postponed arrival times. *)
+  Theorem jitter_FP_compliance `{FP : FP_policy Task} `{JobPreemptable Job}:
+    uniprocessor_model PState ->
+    @respects_FP_policy_at_preemption_point
+      _ _ _ original_arrival _ _ _ jitter_ready_instance arr_seq sched FP ->
+    @respects_FP_policy_at_preemption_point
+      _ _ _ release_as_arrival _ _ _ basic_ready_instance rel_seq sched FP.
+  Proof.
+    move=> UNI COMP j j_hp t ARR_rel PT_rel BL  SCHED_hp.
+    have ARR_arr: arrives_in arr_seq j by rewrite jitter_arrives_in_iff.
+    apply: COMP => //.
+    by rewrite /preemption_time jitter_scheduled_job_at_eq.
+  Qed.
+
+  (** ** Transferred Response-Time Bound *)
+
+  (** Finally, we state the main result, which is the whole point of jitter
+      propagation in the first place: if it is possible to bound response times
+      after release jitter has been folded into the arrival curves, then this
+      implies a response-time bound for the original problem with jitter.
+      This theorem conceptually corresponds to equations (5) and (6) in Audsley
+      et al. (1993), but has been generalized to arbitrary arrival curves.
+
+      - Audsley, N., Burns, A., Richardson, M., Tindell, K., and Wellings,
+        A. (1993). Applying new scheduling theory to static priority preemptive
+        scheduling. Software Engineering Journal, 8(5):284–292.  *)
+  Theorem jitter_response_time_bound :
+    forall tsk R,
+      tsk \in ts ->
+      @task_response_time_bound _ _ release_as_arrival _ _ _ rel_seq sched tsk R ->
+      @task_response_time_bound _ _ original_arrival _ _ _ arr_seq sched tsk (task_jitter tsk + R).
+  Proof.
+    move=> tsk R IN RTB j IN_arr TSK.
+    have IN_rel: arrives_in rel_seq j by rewrite -jitter_arrives_in_iff.
+    move: (RTB j IN_rel TSK).
+    rewrite /job_response_time_bound/job_arrival/release_as_arrival/job_arrival.
+    apply: completion_monotonic.
+    move: TSK; rewrite /job_of_task => /eqP TSK.
+    move: (H_valid_jitter tsk IN j TSK).
+    by lia.
+  Qed.
+
+
+End JitterPropagationFacts.
+