analysis/definitions/sbf/busy.v

+Require Export prosa.util.all.
+Require Export prosa.analysis.definitions.sbf.pred.
+Require Export prosa.analysis.definitions.busy_interval.classical.
+
+(** * SBF within Busy Interval *)
+
+(** In the following, we define a weak notion of a supply bound
+    function, which is a valid SBF only within a busy interval of a
+    task's job. *)
+Section BusySupplyBoundFunctions.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobTask Job Task}.
+
+  (** Consider any kind of processor state model, ... *)
+  Context `{PState : ProcessorState Job}.
+
+  (** ... any valid arrival sequence, and ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... any schedule. *)
+  Variable sched : schedule PState.
+
+  (** Assume a given JLFP policy. *)
+  Context `{JLFP_policy Job}.
+
+  (** Consider a task [tsk]. *)
+  Variable tsk : Task.
+
+  (** We define a predicate that determines whether an interval <<[t1,
+      t2)>> is a busy-interval prefix of a job [j] of task [tsk]. *)
+  Let bi_prefix_of_tsk j t1 t2 :=
+    job_of_task tsk j /\ busy_interval_prefix arr_seq sched j t1 t2.
+
+  (** We say that the SBF is respected in a busy interval w.r.t. task
+      [tsk] if, for any busy interval <<[t1, t2)>> of a job [j ∈ tsk]
+      and a subinterval <<[t1, t) ⊆ [t1, t2)>>, at least [SBF (t -
+      t1)] cumulative supply is provided. *)
+  Definition sbf_respected_in_busy_interval (SBF : duration -> work) :=
+    pred_sbf_respected arr_seq sched bi_prefix_of_tsk SBF.
+
+  (** Next, we define an SBF that is valid within a busy interval. *)
+  Definition valid_busy_sbf (SBF : duration -> work) :=
+    valid_pred_sbf arr_seq sched bi_prefix_of_tsk SBF.
+
+End BusySupplyBoundFunctions.

analysis/definitions/sbf/plain.v

+Require Export prosa.util.all.
+Require Export prosa.analysis.definitions.sbf.pred.
+
+(** * Plain Supply Bound Functions (SBFs) *)
+
+(** ** Parameter Semantics *)
+
+(** In the following, we define the semantics of the classical supply
+    bound functions (SBF). *)
+Section SupplyBoundFunctions.
+
+  (** Consider any type of jobs, ... *)
+  Context {Job : JobType}.
+
+  (** ... any kind of processor state model, ... *)
+  Context `{PState : ProcessorState Job}.
+
+  (** ... any valid arrival sequence, and ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... any schedule. *)
+  Variable sched : schedule PState.
+
+  (** We say that the SBF is respected if, for any time interval <<[t1, t2)>>,
+      at least [SBF (t2 - t1)] cumulative supply is provided within the given
+      interval. In other words, the SBF lower-bounds the provided supply. *)
+  Definition supply_bound_function_respected (SBF : duration -> work) :=
+    pred_sbf_respected arr_seq sched (fun _ _ _ => True) SBF.
+
+  (** We say that a plain SBF is valid iff it is valid w.r.t. a
+      predicate that is always true (i.e., [fun _ _ _ => True]). *)
+  Definition valid_supply_bound_function (SBF : duration -> work) :=
+    valid_pred_sbf arr_seq sched (fun _ _ _ => True) SBF.
+
+  (** Suppose we are given an SBF characterizing the schedule. *)
+  Context {SBF : SupplyBoundFunction}.
+
+  (** Note that the predicate [(fun _ _ _ => True)] can be easily discarded. *)
+  Remark sbf_respected_simplified :
+    supply_bound_function_respected SBF ->
+    forall (j : Job) (t1 t2 : instant),
+      arrives_in arr_seq j ->
+      t1 <= t2 ->
+      SBF (t2 - t1) <= supply_during sched t1 t2.
+  Proof.
+    move => SUP j t1 t2 ARR LE.
+    by apply: (SUP _ _ t2) => //; lia.
+  Qed.
+
+End SupplyBoundFunctions.

analysis/definitions/sbf/pred.v

+Require Export prosa.util.all.
+Require Export prosa.behavior.schedule.
+Require Export prosa.model.processor.supply.
+Require Export prosa.analysis.definitions.sbf.sbf.
+
+(** ** SBF Parameter Semantics *)
+
+(** In the following, we define the semantics of the supply bound
+    functions (SBF) parametrized by a predicate.
+
+    In our development, we use several different types of SBF (such as
+    the classical SBF, SBF within a busy interval, and SBF within an
+    abstract busy interval). The parametrization of the definition
+    with a predicate serves to avoid superfluous duplication.  *)
+Section PredSupplyBoundFunctions.
+
+  (** Consider any type of jobs, ... *)
+  Context {Job : JobType}.
+
+  (** ... any kind of processor state model, ... *)
+  Context `{PState : ProcessorState Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** Consider an arbitrary predicate on jobs and time intervals. *)
+  Variable P : Job -> instant -> instant -> Prop.
+
+  (** We say that the SBF is respected w.r.t. predicate [P] if, for
+      any job [j], an interval <<[t1, t2)>> satisfying [P j], and a
+      subinterval <<[t1, t) ⊆ [t1, t2)>>, at least [SBF (t - t1)]
+      cumulative supply is provided. *)
+  Definition pred_sbf_respected (SBF : duration -> work) :=
+    forall (j : Job) (t1 t2 : instant),
+      arrives_in arr_seq j ->
+      P j t1 t2 ->
+      forall (t : instant),
+        t1 <= t <= t2 ->
+        SBF (t - t1) <= supply_during sched t1 t.
+
+  (** We say that the SBF is valid w.r.t. predicate [P] if two
+      conditions are satisfied: (1) [SBF 0 = 0] and (2) the SBF is
+      respected w.r.t. predicate [P]. *)
+  Definition valid_pred_sbf (SBF : duration -> work) :=
+    SBF 0 = 0
+    /\ pred_sbf_respected SBF.
+
+  (** An SBF is monotone iff for any [δ1] and [δ2] such that [δ1 <=
+      δ2], [SBF δ1 <= SBF δ2]. *)
+  Definition sbf_is_monotone (SBF : duration -> work) :=
+    monotone leq SBF.
+
+  (** In the context of unit-supply processor models, it is known that
+      the amount of supply provided by the processor is bounded by [1]
+      at any time instant. Hence, we can consider a restricted notion
+      of SBF, where the bound can only increase by at most [1] at each
+      time instant. *)
+  Definition unit_supply_bound_function (SBF : duration -> work) :=
+    forall (δ : duration),
+      SBF δ.+1 <= (SBF δ).+1.
+
+  (** Next, suppose we are given an SBF characterizing the schedule. *)
+  Context {SBF : SupplyBoundFunction}.
+
+  (** The assumption [unit_supply_bound_function] together with the
+      introduced validity assumption implies that [SBF δ <= δ] for any [δ]. *)
+  Remark sbf_bounded_by_duration :
+    valid_pred_sbf SBF ->
+    unit_supply_bound_function SBF ->
+    forall δ, SBF δ <= δ.
+  Proof.
+    move => [ZERO _] UNIT; elim.
+    - by rewrite leqn0; apply/eqP.
+    - by move => n; rewrite (leqRW (UNIT _)) ltnS.
+  Qed.
+
+End PredSupplyBoundFunctions.

analysis/definitions/sbf/sbf.v

+Require Export prosa.behavior.job.
+
+(** * Supply Bound Functions (SBF) *)
+
+(** In this module, we define the notion of Supply Bound Functions
+    (SBF), which can be used to reason about the minimum amount of supply
+    provided in a given time interval. *)
+Class SupplyBoundFunction :=
+  supply_bound_function : duration -> work.

restructuring/analysis/schedulability.v → analysis/definitions/schedulability.v

-Require Export rt.restructuring.model.task.absolute_deadline.
-Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export prosa.analysis.facts.behavior.completion.
+Require Import prosa.model.task.absolute_deadline.
 
+(** * Schedulability *)
+
+(** In the following section we define the notion of schedulable
+    task. *)
 Section Task.
+  
+  (** Consider any type of tasks, ... *)
   Context {Task : TaskType}.
-  Context {Job: JobType}.
 
-  Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
+  (** ... any type of jobs associated with these tasks, ... *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
   Context `{JobDeadline Job}.
+  Context `{JobTask Job Task}.
 
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  (** ... and any kind of processor state. *)
+  Context {PState : ProcessorState Job}.
 
   (** Consider any job arrival sequence... *)
   Variable arr_seq: arrival_sequence Job.
@@ -17,63 +26,46 @@ Section Task.
   (** ...and any schedule of these jobs. *)
   Variable sched: schedule PState.
 
-  (** Let tsk be any task that is to be analyzed. *)
+  (** Let [tsk] be any task that is to be analyzed. *)
   Variable tsk: Task.
 
-  (** Then, we say that R is a response-time bound of tsk in this schedule ... *)
+  (** Then, we say that R is a response-time bound of [tsk] in this schedule ... *)
   Variable R: duration.
 
-  (** ... iff any job j of tsk in this arrival sequence has
-         completed by (job_arrival j + R). *)
+  (** ... iff any job [j] of [tsk] in this arrival sequence has
+         completed by [job_arrival j + R]. *)
   Definition task_response_time_bound :=
     forall j,
       arrives_in arr_seq j ->
-      job_task j = tsk ->
+      job_of_task tsk j ->
       job_response_time_bound sched j R.
 
   (** We say that a task is schedulable if all its jobs meet their deadline *)
   Definition schedulable_task :=
     forall j,
       arrives_in arr_seq j ->
-      job_task j = tsk ->
+      job_of_task tsk j ->
       job_meets_deadline sched j.
+  
 End Task.
 
-Section TaskSet.
-  Context {Task : TaskType}.
-  Context {Job: JobType}.
-
-  Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
-  Context `{JobDeadline Job}.
-
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
-
-  Variable ts : {set Task}.
-
-  (** Consider any job arrival sequence... *)
-  Variable arr_seq: arrival_sequence Job.
-
-  (** ...and any schedule of these jobs. *)
-  Variable sched: schedule PState.
-
-  (** We say that a task set is schedulable if all its tasks are schedulable *)
-  Definition schedulable_taskset :=
-    forall tsk, tsk \in ts -> schedulable_task arr_seq sched tsk.
-End TaskSet.
-
-Section Schedulability.
-  (** We can infer schedulability from a response-time bound of a task. *)
+(** In this section we infer schedulability from a response-time bound
+    of a task. *)
+Section Schedulability.  
 
+  (** Consider any type of tasks, ... *)
   Context {Task : TaskType}.
-  Context {Job: JobType}.
-
   Context `{TaskDeadline Task}.
-  Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
 
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  (** ... any type of jobs associated with these tasks, ... *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobTask Job Task}.
 
+  (** ... and any kind of processor state. *)
+  Context {PState : ProcessorState Job}.
+  
   (** Consider any job arrival sequence... *)
   Variable arr_seq: arrival_sequence Job.
 
@@ -83,16 +75,16 @@ Section Schedulability.
   (** Assume that jobs don't execute after completion. *)
   Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
 
-  (** Let tsk be any task that is to be analyzed. *)
+  (** Let [tsk] be any task that is to be analyzed. *)
   Variable tsk: Task.
 
-  (** Given  a response-time bound of tsk in this schedule no larger than its deadline, ... *)
+  (** Given  a response-time bound of [tsk] in this schedule no larger than its deadline, ... *)
   Variable R: duration.
 
   Hypothesis H_R_le_deadline: R <= task_deadline tsk.
   Hypothesis H_response_time_bounded: task_response_time_bound arr_seq sched tsk R.
 
-  (** ...then tsk is schedulable. *)
+  (** ...then [tsk] is schedulable. *)
   Lemma schedulability_from_response_time_bound:
     schedulable_task arr_seq sched tsk.
   Proof.
@@ -100,8 +92,9 @@ Section Schedulability.
     rewrite /job_meets_deadline.
     apply completion_monotonic with (t := job_arrival j + R);
       [ | by apply H_response_time_bounded].
-    rewrite /job_deadline leq_add2l JOBtsk.
-      by erewrite leq_trans; eauto.
+    rewrite /job_deadline leq_add2l.
+    move: JOBtsk => /eqP ->.
+    by erewrite leq_trans; eauto.
   Qed.
 
 End Schedulability.
@@ -112,13 +105,15 @@ End Schedulability.
     given schedule and one w.r.t. all jobs that arrive in a given
     arrival sequence. *)
 Section AllDeadlinesMet.
-
+  
   (** Consider any given type of jobs... *)
-  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobDeadline Job}.
 
   (** ... any given type of processor states. *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** We say that all deadlines are met if every job scheduled at some
      point in the schedule meets its deadline. Note that this is a
@@ -151,8 +146,8 @@ Section AllDeadlinesMet.
   End DeadlinesOfArrivals.
 
   (** We observe that the latter definition, assuming a schedule in
-     which all jobs come from the arrival sequence, implies the former
-     definition. *)
+      which all jobs come from the arrival sequence, implies the
+      former definition. *)
   Lemma all_deadlines_met_in_valid_schedule:
     forall arr_seq sched,
       jobs_come_from_arrival_sequence sched arr_seq ->

analysis/definitions/schedule_prefix.v

+Require Export prosa.behavior.ready.
+Require Export prosa.util.nat.
+
+(** We define the notion of prefix-equivalence of schedules. *)
+
+Section PrefixDefinition.
+
+  (** For any type of jobs... *)
+  Context {Job : JobType}.
+
+  (** ... and any kind of processor model, ... *)
+  Context {PState: ProcessorState Job}.
+
+  (** ... two schedules share an identical prefix if they are pointwise
+          identical (at least) up to a fixed horizon. *)
+  Definition identical_prefix (sched sched' : schedule PState) (horizon : instant) :=
+    forall t,
+      t < horizon ->
+      sched t = sched' t.
+
+  (** In other words, two schedules with a shared prefix are completely
+      interchangeable w.r.t. whether a job is scheduled (in the prefix). *)
+  Fact identical_prefix_scheduled_at :
+    forall sched sched' h,
+      identical_prefix sched sched' h ->
+      forall j t,
+        t < h ->
+        scheduled_at sched j t = scheduled_at sched' j t.
+  Proof.
+    move=> sched sched' h IDENT j t LT_h.
+    now rewrite /scheduled_at (IDENT t LT_h).
+  Qed.
+
+  (** Trivially, any prefix of an identical prefix is also an identical
+      prefix. *)
+  Fact identical_prefix_inclusion :
+    forall sched sched' h h',
+      h' <= h ->
+      identical_prefix sched sched' h -> identical_prefix sched sched' h'.
+  Proof. by move=> sched sched' h h' h'_le_h + t t_lt_h'; apply; apply: leq_trans h'_le_h. Qed.
+
+End PrefixDefinition.

analysis/definitions/service.v

+Require Export prosa.behavior.service.
+
+(** * Service Definitions *)
+
+(** In this section, we define a set of jobs that receive service at a
+    given time. *)
+Section ServedAt.
+
+  (** Consider any kind of jobs and any kind of processor state. *)
+  Context {Job : JobType} {PState : ProcessorState Job}.
+
+  (** Consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** The set of jobs served at time [t] can be obtained by filtering
+      the set of all jobs that arrive at or before time [t]. *)
+  Definition served_jobs_at (t : instant) :=
+    [seq j <- arrivals_up_to arr_seq t | receives_service_at sched j t].
+
+  (** For the special case of uniprocessors, we define a convenience
+      wrapper that reduces the sequence of scheduled jobs to an
+      [option Job]. *)
+  Definition served_job_at t := ohead (served_jobs_at t).
+
+End ServedAt.

analysis/definitions/service_inversion/busy_prefix.v

+Require Export prosa.model.priority.classes.
+Require Export prosa.analysis.facts.behavior.completion.
+Require Export prosa.analysis.definitions.service.
+Require Export prosa.analysis.definitions.service_inversion.pred.
+Require Export prosa.analysis.definitions.busy_interval.classical.
+
+(** * Service Inversion Bounded *)
+(** In this section, we define the notion of bounded cumulative
+    service inversion in a busy interval prefix. *)
+Section ServiceInversion.
+
+  (** 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}.
+
+  (** Next, consider _any_ kind of processor state model, ... *)
+  Context {PState : ProcessorState Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Assume a given JLFP policy. *)
+  Context `{JLFP_policy Job}.
+
+  (** If the priority inversion experienced by job [j] depends on its
+      relative arrival time w.r.t. the beginning of its busy interval
+      at a time [t1], we say that the service inversion of job [j] is
+      bounded by a function [B : duration -> duration] if the
+      cumulative service inversion within any busy interval prefix is
+      bounded by [B (job_arrival j - t1)]. *)
+  Definition service_inversion_of_job_is_bounded_by (j : Job) (B : duration -> duration) :=
+    pred_service_inversion_of_job_is_bounded_by
+      arr_seq sched (busy_interval_prefix arr_seq sched) j B.
+
+  (** We say that task [tsk] has bounded service inversion if all its
+      jobs have cumulative service inversion bounded by function [B :
+      duration -> duration], where [B] may depend on jobs' relative
+      arrival times w.r.t. the beginning of the busy interval. *)
+  Definition service_inversion_is_bounded_by (tsk : Task) (B : duration -> duration) :=
+    pred_service_inversion_is_bounded_by
+      arr_seq sched (busy_interval_prefix arr_seq sched) tsk B.
+
+End ServiceInversion.

analysis/definitions/service_inversion/pred.v

+Require Export prosa.model.priority.classes.
+Require Export prosa.analysis.facts.behavior.completion.
+Require Export prosa.analysis.definitions.service.
+
+(** * Service Inversion *)
+(** In this section, we define the notion of service inversion for
+    arbitrary processors. *)
+Section ServiceInversion.
+
+  (** 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}.
+
+  (** Next, consider _any_ kind of processor state model, ... *)
+  Context {PState : ProcessorState Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Assume a given JLDP policy. *)
+  Context `{JLDP_policy Job}.
+
+  (** Consider an arbitrary predicate on time intervals. *)
+  Variable P : Job -> instant -> instant -> Prop.
+
+  (** Consider a job [j]. *)
+  Variable j : Job.
+
+  (** We say that the job incurs service inversion if it has higher
+      priority than the job receiving service. Note that this
+      definition is oblivious to whether job [j] is ready. Therefore,
+      it may not apply as intuitively expected in models with jitter
+      or self-suspensions. Further generalization of the concept is
+      likely necessary to efficiently analyze models in which jobs may
+      be pending without being ready. *)
+  Definition service_inversion (t : instant) :=
+    (j \notin served_jobs_at arr_seq sched t)
+    && has (fun jlp => ~~ hep_job_at t jlp j) (served_jobs_at arr_seq sched t).
+
+  (** Then we compute the cumulative service inversion incurred by a
+      job within some time interval <<[t1, t2)>>. *)
+  Definition cumulative_service_inversion (t1 t2 : instant) :=
+    \sum_(t1 <= t < t2) service_inversion t.
+
+  (** For proof purposes, it is often useful to bound the cumulative
+      service interference in a time interval <<[t1, t2)>> that
+      satisfies a given predicate (e.g., <<[t1, t2)>> is a busy
+      interval prefix). To this end, we say that the cumulative
+      service inversion of job [j] is bounded by a function [B :
+      duration -> duration] w.r.t. to predicate [P] iff, for any
+      interval <<[t1, t2)>> that satisfies [P j], the cumulative
+      priority inversion in <<[t1, t2)>> is bounded by [B (job_arrival
+      j - t1)]. *)
+  Definition pred_service_inversion_of_job_is_bounded_by (B : duration -> duration) :=
+    forall (t1 t2 : instant),
+      P j t1 t2 ->
+      cumulative_service_inversion t1 t2 <= B (job_arrival j - t1).
+
+End ServiceInversion.
+
+(** In this section, we define a notion of the bounded service
+    inversion for tasks. *)
+Section TaskServiceInversionBound.
+
+  (** 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 processor state model, ... *)
+  Context {PState : ProcessorState Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** Assume a given JLDP policy. *)
+  Context `{JLDP_policy Job}.
+
+  (** Consider an arbitrary predicate on jobs and time intervals. *)
+  Variable P : Job -> instant -> instant -> Prop.
+
+  (** Consider an arbitrary task [tsk]. *)
+  Variable tsk : Task.
+  
+  (** We say that task [tsk] has bounded service inversion if all its
+      jobs have cumulative service inversion bounded by function [B :
+      duration -> duration]. *)
+  Definition pred_service_inversion_is_bounded_by (B : duration -> duration) :=
+    forall (j : Job),
+      arrives_in arr_seq j ->
+      job_of_task tsk j ->
+      job_cost j > 0 ->
+      pred_service_inversion_of_job_is_bounded_by arr_seq sched P j B.
+
+End TaskServiceInversionBound.

analysis/definitions/tardiness.v

+Require Export prosa.analysis.definitions.schedulability.
+
+(** * Tardiness *)
+
+(** In the following section we define the notion of bounded tardiness, 
+    i.e., an upper-bound on the difference between the response time of 
+    any job of a task and its relative deadline. *)
+Section Tardiness.
+  
+  (** Consider any type of tasks and its deadline, ... *)
+  Context {Task : TaskType}.
+  Context `{TaskDeadline Task}.
+
+  (** ... any type of jobs associated with these tasks, ... *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobTask Job Task}.
+
+  (** ... and any kind of processor state. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Further, consider any job arrival sequence... *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (** ...and any schedule of these jobs. *)
+  Variable sched: schedule PState.
+
+  (** Let [tsk] be any task that is to be analyzed. *)
+  Variable tsk: Task.
+
+  (** Then, we say that B is a tardiness bound of [tsk] in this schedule ... *)
+  Variable B: duration.
+
+  (** ... iff any job [j] of [tsk] in the arrival sequence has
+         completed no more that [B] time units after its deadline. *)
+  Definition task_tardiness_is_bounded arr_seq sched tsk B :=
+    task_response_time_bound arr_seq sched tsk (task_deadline tsk + B).
+  
+End Tardiness.

analysis/definitions/task_schedule.v

+Require Export prosa.model.task.concept.
+Require Export prosa.analysis.definitions.service.
+Require Export prosa.model.schedule.scheduled.
+
+(** * Schedule and Service of task *)
+(** In this section we define properties of the schedule and service
+    of a task. *)
+Section ScheduleAndServiceOfTask.
+
+  (** 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 of such jobs. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** Let [sched] be any kind of schedule *)
+  Context {PState : ProcessorState Job}.
+  Variable sched : schedule PState.
+
+  (** Let [tsk] be any task. *)
+  Variable tsk : Task.
+
+  (** We define a set of jobs of task [tsk] that are scheduled at time
+      [t]. *)
+  Definition scheduled_jobs_of_task_at (t : instant) :=
+    [seq j <- scheduled_jobs_at arr_seq sched t | job_of_task tsk j].
+
+  (** Next we define whether task [tsk] is scheduled at time [t]. *)
+  Definition task_scheduled_at (t : instant) :=
+    scheduled_jobs_of_task_at t != [::].
+
+  (** We define the instantaneous service of [tsk] as the total
+      instantaneous service of all jobs of this task scheduled at time
+      [t]. *)
+  Definition task_service_at (t : instant) :=
+    \sum_(j <- scheduled_jobs_of_task_at t) service_at sched j t.
+
+  (** Based on the notion of instantaneous service, we define the
+      cumulative service received by [tsk] during any interval <<[t1,
+      t2)>> ... *)
+  Definition task_service_during (t1 t2 : instant) :=
+    \sum_(t1 <= t < t2) task_service_at t.
+
+  (** ...and the cumulative service received by [tsk] up to time [t2],
+      i.e., in the interval <<[0, t2)>>. *)
+  Definition task_service (t2 : instant) := task_service_during 0 t2.
+
+  (** Similarly, we define a set of jobs of task [tsk] receiving
+      service at time [t]. *)
+  Definition served_jobs_of_task_at (t : instant) :=
+    [seq j <- scheduled_jobs_of_task_at t | receives_service_at sched j t].
+
+  (** Next, we define whether [tsk] is served at time [t]. *)
+  Definition task_served_at (t : instant) :=
+    served_jobs_of_task_at t != [::].
+
+End ScheduleAndServiceOfTask.

analysis/definitions/work_bearing_readiness.v

+Require Export prosa.model.priority.classes.
+
+(** * Work-Bearing Readiness *)
+
+(** In this module, we introduce a property of readiness models that
+    is called work-bearing readiness. Work-bearing readiness extracts
+    the useful property of the classic readiness model stating that,
+    if there is a job pending at a time instant [t], then there also
+    exists a job that is ready at time [t]. In other words, we say
+    that a readiness model is a work-bearing readiness model if, for
+    any job [j] and any time instant [t], if job [j] is pending but
+    not ready at [t], then there is a job with higher or equal
+    priority [j_hp] that is both pending and ready at time [t]. *)
+
+Section WorkBearingReadiness.
+
+  (** Consider any type of job associated with any type of tasks ... *)
+  Context {Job : JobType} {Task : TaskType} `{JobArrival Job} `{JobCost Job}.
+
+  (** ... and any kind of processor state. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Further, allow for any notion of job readiness. *)
+  Context {jr : JobReady Job PState}.
+
+  (** Consider any job arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... any schedule of these jobs, ... *)
+  Variable sched : schedule PState.
+
+  (** ... and a JLFP policy that indicates a higher-or-equal priority relation. *)
+  Context `{JLFP_policy Job}.
+
+  (** If a job [j] is pending at a time instant [t], then (even if it
+      is not ready at time [t]) there is a job [j_hp] with
+      higher-or-equal priority that is ready at time instant [t]. *)
+  Definition work_bearing_readiness :=
+    forall (j : Job) (t : instant),
+      arrives_in arr_seq j ->
+      pending sched j t ->
+      exists j_hp,
+        arrives_in arr_seq j_hp /\
+        job_ready sched j_hp t /\
+        hep_job j_hp j.
+
+End WorkBearingReadiness.

analysis/definitions/workload/bounded.v

+Require Export prosa.model.aggregate.workload.
+Require Export prosa.analysis.definitions.busy_interval.classical.
+
+(** * Workload Bound in an Interval Starting with Quiet Time *)
+(** In this section, we define the notion of a bound on the total
+    workload from higher-or-equal-priority tasks in an interval that
+    starts with a quiet time. *)
+Section WorkloadBound.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+  Context `{JobTask Job Task}.
+
+  (** Consider any kind of processor model. *)
+  Context `{PState : ProcessorState Job}.
+
+  (** Consider a JLFP policy that indicates a higher-or-equal-priority
+      relation. *)
+  Context {JLFP : JLFP_policy Job}.
+
+  (** Consider an arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and a schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Let [tsk] be any task. *)
+  Variable tsk : Task.
+
+  (** We say that [B : duration -> duration -> work] is a bound on the
+      higher-or-equal-priority workload of tasks different from [tsk]
+      iff, for any job [j ∈ tsk] and any interval <<[t1, t1 + Δ)>>
+      that starts with a quiet time (w.r.t. job [j]), the total
+      workload of higher-or-equal-priority tasks distinct from [tsk]
+      in the interval <<[t1, t1 + Δ)>> is bounded by
+      [B (job_arrival j - t1) Δ]. *)
+  Definition athep_workload_is_bounded (B : duration -> duration -> work) :=
+    forall (j : Job) (t1 : instant) (Δ : duration),
+      job_cost_positive j ->
+      job_of_task tsk j ->
+      quiet_time arr_seq sched j t1 ->
+      workload_of_jobs (another_task_hep_job^~ j) (arrivals_between arr_seq t1 (t1 + Δ))
+      <= B (job_arrival j - t1) Δ.
+
+End WorkloadBound.

analysis/definitions/workload/edf_athep_bound.v

+Require Export prosa.analysis.definitions.request_bound_function.
+
+(** * Bound on Higher-or-Equal Priority Workload under EDF Scheduling  *)
+
+(** In this file, we define an upper bound on workload incurred by a
+    job from jobs with higher-or-equal priority that come from other
+    tasks under EDF scheduling. *)
+Section EDFWorkloadBound.
+
+  (** Consider any type of tasks, each characterized by a WCET
+      [task_cost], and an arrival curve [max_arrivals]. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskDeadline Task}.
+  Context `{MaxArrivals Task}.
+
+  (** Consider an arbitrary task set [ts] ... *)
+  Variable ts : seq Task.
+
+  (** ... and a task [tsk]. *)
+  Variable tsk : Task.
+
+  (** For brevity, let's denote the relative deadline of a task as [D] ... *)
+  Let D tsk := task_deadline tsk.
+
+  (** ... and let's use the abbreviation [rbf] for the task
+      request-bound function. *)
+  Let rbf := task_request_bound_function.
+
+  (** Finally, we define an upper bound on workload received from jobs
+      with higher-than-or-equal priority that come from other
+      tasks. *)
+  Definition bound_on_athep_workload A Δ :=
+    \sum_(tsk_o <- ts | tsk_o != tsk)
+     rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+
+End EDFWorkloadBound.

analysis/definitions/workload/elf_athep_bound.v

+Require Export prosa.analysis.definitions.request_bound_function.
+Require Import prosa.model.priority.elf.
+
+(** * Bound on Higher-or-Equal Priority Workload under ELF Scheduling  *)
+
+(** In this file, we define an upper bound on workload incurred by a
+    job from jobs with higher-or-equal priority that come from other
+    tasks under ELF scheduling. *)
+Section ELFWorkloadBound.
+
+  (** Consider any type of tasks, each characterized by a WCET
+      [task_cost], and an arrival curve [max_arrivals]. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{MaxArrivals Task}.
+
+  (** Suppose the tasks have relative priority points. *)
+  Context `{PriorityPoint Task}.
+
+  (** Now consider any task set [ts]. *)
+  Variable ts : seq Task.
+
+  (** Consider any FP Policy. *)
+  Context {FP : FP_policy Task}.
+
+  (** Now we define, given the arrival offset [A], the length of the interval in which
+     a higher or equal priority job from a task [tsk_o] in the same priority band as [tsk]
+     may arrive. *)
+  Definition ep_task_interfering_interval_length (tsk tsk_o : Task) (A : duration) :=
+    ((A + ε)%:R + task_priority_point tsk - task_priority_point tsk_o)%R.
+
+  (** Using the above definition, we now define a bound on the higher-or-equal priority workload
+      from tasks in the same priority band as [tsk]. *)
+  Definition bound_on_ep_task_workload (tsk : Task) (A : duration) (delta : duration) :=
+    let rbf_duration (tsk_o : Task) := minn `|Num.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| delta in
+      \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk))
+        task_request_bound_function tsk_o (rbf_duration tsk_o).
+
+  (** Next we define a bound on the higher-priority workload from tasks in
+      higher priority bands than [tsk]. *)
+  Definition bound_on_hp_task_workload (tsk : Task) (delta : duration) :=
+    total_hp_request_bound_function_FP ts tsk delta.
+
+  (** Finally, we define an upper bound on the workload received from jobs
+      with higher-than-or-equal priority that come from other
+      tasks. *)
+  Definition bound_on_athep_workload tsk A delta :=
+    bound_on_hp_task_workload tsk delta + bound_on_ep_task_workload tsk A delta.
+
+End ELFWorkloadBound.

analysis/facts/SBF.v

+Require Export prosa.analysis.definitions.sbf.pred.
+Require Export prosa.analysis.facts.behavior.supply.
+Require Export prosa.model.task.concept.
+
+(** In this section, we prove some useful facts about SBF. *)
+Section SupplyBoundFunctionLemmas.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of unit-supply processor state model, ... *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+
+  (** ... any valid arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** In the following section, we prove a lemma about switching a
+      predicate inside of [valid_pred_sbf]. *)
+  Section SBFChangePred.
+
+    (** Consider an SBF ... *)
+    Context {SBF : SupplyBoundFunction}.
+
+    (** ... and two predicates [P1] and [P2] such that, for any job [j]
+        and a time interval <<[t1, t2)>>, [P2 j t1 t2] implies [P1 j t1 t2]. *)
+    Variables P1 P2 : Job -> instant -> instant -> Prop.
+    Hypothesis H_p2_implies_p1 :
+      forall j t1 t2,
+        arrives_in arr_seq j ->
+        P2 j t1 t2 -> P1 j t1 t2.
+
+    (** Then if [SBF] is a valid SBF w.r.t. predicate [P1], then [SBF]
+        is a valid SBF w.r.t. predicate [P2]. *)
+    Lemma valid_pred_sbf_switch_predicate :
+      valid_pred_sbf arr_seq sched P1 SBF ->
+      valid_pred_sbf arr_seq sched P2 SBF.
+    Proof.
+      move=> VAL; split; first by apply VAL.
+      move=> j t1 t2 ARR P2j t NEQ.
+      by eapply VAL => //.
+    Qed.
+
+  End SBFChangePred.
+
+  (** Consider an arbitrary predicate on jobs and time intervals. *)
+  Variable P : Job -> instant -> instant -> Prop.
+
+  (** Consider a supply-bound function [SBF] that is valid w.r.t. the
+      predicate [P]. That is, (1) [SBF 0 = 0] and (2) for any job [j],
+      an interval <<[t1, t2)>> satisfying [P j], and a subinterval
+      <<[t1, t) ⊆ [t1, t2)>>, the supply produced during the time
+      interval <<[t1, t)>> is at least [SBF (t - t1)]. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_pred_sbf arr_seq sched P SBF.
+
+  (** In this section, we show a simple upper bound on the blackout
+      during an interval of length [Δ]. *)
+  Section BlackoutBound.
+
+    (** Consider any job [j]. *)
+    Variable j : Job.
+    Hypothesis H_arrives_in : arrives_in arr_seq j.
+
+    (** Consider an interval <<[t1, t2)>> satisfying [P j]. *)
+    Variables t1 t2 : instant.
+    Hypothesis H_P_interval : P j t1 t2.
+
+    (** Consider an arbitrary duration [Δ] such that [t1 + Δ <= t2]. *)
+    Variable Δ : duration.
+    Hypothesis H_subinterval : t1 + Δ <= t2.
+
+    (** We show that the total blackout time during an interval of
+        length [Δ] is bounded by [Δ - SBF Δ]. *)
+    Lemma blackout_during_bound :
+      blackout_during sched t1 (t1 + Δ) <= Δ - SBF Δ.
+    Proof.
+      rewrite blackout_during_complement // leq_sub => //.
+      rewrite -(leqRW (snd H_valid_SBF _ _ _ _ _ _ _)).
+      { by have -> : (t1 + Δ) - t1 = Δ by lia. }
+      { by apply H_arrives_in. }
+      { by eapply H_P_interval. }
+      { lia. }
+     Qed.
+
+  End BlackoutBound.
+
+  (** In the following section, we prove a few facts about _unit_ SBF. *)
+  Section UnitSupplyBoundFunctionLemmas.
+
+    (** In addition, let us assume that [SBF] is a unit-supply SBF.
+        That is, [SBF] makes steps of at most one. *)
+    Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+    (** We prove that the complement of such an SBF (i.e., [fun Δ => Δ -
+        SBF Δ]) is monotone. *)
+    Lemma complement_SBF_monotone :
+      forall Δ1 Δ2,
+        Δ1 <= Δ2 ->
+        Δ1 - SBF Δ1 <= Δ2 - SBF Δ2.
+    Proof.
+      move => Δ1 Δ2 LE; interval_to_duration Δ1 Δ2 k.
+      elim: k => [|δ IHδ]; first by rewrite addn0.
+      by rewrite (leqRW IHδ) addnS (leqRW (H_unit_SBF _)); lia.
+    Qed.
+
+  End UnitSupplyBoundFunctionLemmas.
+
+End SupplyBoundFunctionLemmas.

analysis/facts/behavior/all.v

+Require Export prosa.analysis.facts.behavior.service.
+Require Export prosa.analysis.facts.behavior.completion.
+Require Export prosa.analysis.facts.behavior.arrivals.
+Require Export prosa.analysis.facts.behavior.deadlines.

analysis/facts/behavior/arrivals.v

+Require Export prosa.behavior.all.
+Require Export prosa.util.all.
+Require Export prosa.model.task.arrivals.
+
+(** * Arrival Sequence *)
+
+(** First, we relate the stronger to the weaker arrival predicates. *)
+Section ArrivalPredicates.
+
+  (** Consider any kinds of jobs with arrival times. *)
+  Context {Job : JobType} `{JobArrival Job}.
+
+  (** A job that arrives in some interval <<[t1, t2)>> certainly arrives before
+      time [t2]. *)
+  Lemma arrived_between_before:
+    forall j t1 t2,
+      arrived_between j t1 t2 ->
+      arrived_before j t2.
+  Proof. by move=> ? ? ? /andP[]. Qed.
+
+  (** A job that arrives before a time [t] certainly has arrived by time
+      [t]. *)
+  Lemma arrived_before_has_arrived:
+    forall j t,
+      arrived_before j t ->
+      has_arrived j t.
+  Proof. move=> ? ?; exact: ltnW. Qed.
+
+  (** Furthermore, we restate a common hypothesis to make its
+      implication easier to discover. *)
+  Lemma consistent_times_valid_arrival :
+    forall arr_seq,
+      valid_arrival_sequence arr_seq -> consistent_arrival_times arr_seq.
+  Proof. by move=> ? []. Qed.
+
+  (** We restate another common hypothesis to make its implication
+      easier to discover. *)
+  Lemma uniq_valid_arrival :
+    forall arr_seq,
+      valid_arrival_sequence arr_seq -> arrival_sequence_uniq arr_seq.
+  Proof. by move=> ? []. Qed.
+
+End ArrivalPredicates.
+
+(** In this section, we relate job readiness to [has_arrived]. *)
+Section Arrived.
+
+  (** Consider any kinds of jobs and any kind of processor state. *)
+  Context {Job : JobType} {PState : ProcessorState Job}.
+
+  (** Consider any schedule... *)
+  Variable sched : schedule PState.
+
+  (** ...and suppose that jobs have a cost, an arrival time, and a
+      notion of readiness. *)
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+  Context {jr : JobReady Job PState}.
+
+  (** First, we note that readiness models are by definition consistent
+      w.r.t. [pending]. *)
+  Lemma any_ready_job_is_pending:
+    forall j t,
+      job_ready sched j t -> pending sched j t.
+  Proof. move: jr => [? +] /= ?; exact. Qed.
+
+  (** Next, we observe that a given job must have arrived to be ready... *)
+  Lemma ready_implies_arrived :
+    forall j t, job_ready sched j t -> has_arrived j t.
+  Proof. by move=> ? ? /any_ready_job_is_pending => /andP[]. Qed.
+
+  (** ...and lift this observation also to the level of whole schedules. *)
+  Lemma jobs_must_arrive_to_be_ready:
+    jobs_must_be_ready_to_execute sched -> jobs_must_arrive_to_execute sched.
+  Proof. move=> READY ? ? ?; exact/ready_implies_arrived/READY. Qed.
+
+  (** Furthermore, in a valid schedule, jobs must arrive to execute. *)
+  Corollary valid_schedule_implies_jobs_must_arrive_to_execute :
+    forall arr_seq,
+      valid_schedule sched arr_seq -> jobs_must_arrive_to_execute sched.
+  Proof. move=> ? [? ?]; exact: jobs_must_arrive_to_be_ready. Qed.
+
+  (** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
+  Corollary backlogged_implies_arrived:
+    forall j t,
+      backlogged sched j t -> has_arrived j t.
+  Proof. move=> ? ? /andP[? ?]; exact: ready_implies_arrived. Qed.
+
+  (** Similarly, since backlogged jobs are by definition pending, any
+      backlogged job must be incomplete. *)
+  Lemma backlogged_implies_incomplete:
+    forall j t,
+      backlogged sched j t -> ~~ completed_by sched j t.
+  Proof. by move=> ? ? /andP[/any_ready_job_is_pending /andP[]]. Qed.
+
+  (** Finally, we restate common hypotheses on the well-formedness of
+      schedules to make their implications more easily
+      discoverable. First, on the readiness of scheduled jobs, ... *)
+  Lemma job_scheduled_implies_ready :
+    jobs_must_be_ready_to_execute sched ->
+    forall j t,
+      scheduled_at sched j t -> job_ready sched j t.
+  Proof. exact. Qed.
+
+  (** ... second, on the origin of scheduled jobs, and ... *)
+  Lemma valid_schedule_jobs_come_from_arrival_sequence :
+    forall arr_seq,
+      valid_schedule sched arr_seq ->
+      jobs_come_from_arrival_sequence sched arr_seq.
+  Proof. by move=> ? []. Qed.
+
+  (** ... third, on the readiness of jobs in valid schedules. *)
+  Lemma valid_schedule_jobs_must_be_ready_to_execute :
+    forall arr_seq,
+      valid_schedule sched arr_seq -> jobs_must_be_ready_to_execute sched.
+  Proof. by move=> ? []. Qed.
+
+End Arrived.
+
+(** In this section, we establish useful facts about arrival sequence prefixes. *)
+Section ArrivalSequencePrefix.
+
+  (** Consider any kind of tasks and jobs. *)
+  Context {Job: JobType}.
+  Context {Task : TaskType}.
+  Context `{JobArrival Job}.
+  Context `{JobTask Job Task}.
+
+  (** Consider any job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (** We begin with basic lemmas for manipulating the sequences. *)
+  Section Composition.
+
+    (** We show that the set of arriving jobs can be split
+         into disjoint intervals. *)
+    Lemma arrivals_between_cat:
+      forall t1 t t2,
+        t1 <= t ->
+        t <= t2 ->
+        arrivals_between arr_seq t1 t2 =
+        arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
+    Proof. by move=> ? ? ? ? ?; rewrite -big_cat_nat. Qed.
+
+    (** We also prove a stronger version of the above lemma
+     in the case of arrivals that satisfy a predicate [P]. *)
+    Lemma arrivals_P_cat:
+      forall P t t1 t2,
+        t1 <= t < t2 ->
+        arrivals_between_P arr_seq P t1 t2 =
+        arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2.
+    Proof.
+      move=> P t t1 t2.
+      by move=> /andP[? ?]; rewrite -filter_cat -arrivals_between_cat// ltnW.
+    Qed.
+
+    (** The same observation applies to membership in the set of
+         arrived jobs. *)
+    Lemma arrivals_between_mem_cat:
+      forall j t1 t t2,
+        t1 <= t ->
+        t <= t2 ->
+        j \in arrivals_between arr_seq t1 t2 =
+        (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
+    Proof. by move=> ? ? ? ? ? ?; rewrite -arrivals_between_cat. Qed.
+
+    (** We observe that we can grow the considered interval without
+         "losing" any arrived jobs, i.e., membership in the set of arrived jobs
+         is monotonic. *)
+    Lemma arrivals_between_sub :
+      forall j t1 t1' t2 t2',
+        t1' <= t1 ->
+        t2 <= t2' ->
+        j \in arrivals_between arr_seq t1 t2 ->
+        j \in arrivals_between arr_seq t1' t2'.
+    Proof.
+      move=> j t1 t1' t2 t2' t1'_le_t1 t2_le_t2' j_in.
+      have /orP[t2_le_t1|t1_le_t2] := leq_total t2 t1.
+      { by move: j_in; rewrite /arrivals_between big_geq. }
+      rewrite (arrivals_between_mem_cat _ _ t1)// ?mem_cat.
+      2:{ exact: leq_trans t2_le_t2'. }
+      rewrite [X in _ || X](arrivals_between_mem_cat _ _ t2)// mem_cat.
+      by rewrite j_in orbT.
+    Qed.
+
+  End Composition.
+
+  (** Next, we relate the arrival prefixes with job arrival times. *)
+  Section ArrivalTimes.
+
+    (** Assume that job arrival times are consistent. *)
+    Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
+
+    (** To make the hypothesis and its implication easier to discover,
+        we restate it as a trivial lemma. *)
+    Lemma job_arrival_arrives_at :
+      forall {j t},
+        arrives_at arr_seq j t -> job_arrival j = t.
+    Proof. exact: H_consistent_arrival_times. Qed.
+
+    (** Similarly, to simplify subsequent proofs, we restate the
+        [H_consistent_arrival_times] assumption as a trivial
+        corollary. *)
+    Lemma job_arrival_at :
+      forall {j t},
+        j \in arrivals_at arr_seq t -> job_arrival j = t.
+    Proof. exact: H_consistent_arrival_times. Qed.
+
+    (** Next, we  prove that if [j] is a part of the arrival sequence,
+        then the converse of the above also holds. *)
+    Lemma job_in_arrivals_at :
+      forall j t,
+        arrives_in arr_seq j ->
+        job_arrival j = t ->
+        j \in arrivals_at arr_seq t.
+    Proof.
+      move => j t [t' IN] => /eqP.
+      apply contraTT => /negP NOTIN.
+      apply /neqP => ARR.
+      have ARR' := (H_consistent_arrival_times _ t' IN).
+      by move: IN; rewrite -ARR' ARR.
+    Qed.
+
+    (** To begin with actual properties, we observe that any job in
+        the set of all arrivals between time instants [t1] and [t2]
+        must arrive in the interval <<[t1,t2)>>. *)
+    Lemma job_arrival_between :
+      forall {j t1 t2},
+        j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j < t2.
+    Proof. by move=> ? ? ? /mem_bigcat_nat_exists[i [/job_arrival_at <-]]. Qed.
+
+    (** For convenience, we restate the left bound of the above lemma... *)
+    Corollary job_arrival_between_ge :
+      forall {j t1 t2},
+        j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j.
+    Proof. by move=> ? ? ? /job_arrival_between/andP[]. Qed.
+
+    (** ... as well as the right bound separately as corollaries. *)
+    Corollary job_arrival_between_lt :
+      forall {j t1 t2},
+        j \in arrivals_between arr_seq t1 t2 -> job_arrival j < t2.
+    Proof. by move=> ? ? ? /job_arrival_between/andP[]. Qed.
+
+    (** Consequently, if we filter the list of arrivals in an interval
+        <<[t1,t2)>> with an arrival-time threshold less than [t1], we are
+        left with an empty list. *)
+    Lemma arrivals_between_filter_nil :
+      forall t1 t2 t,
+        t < t1 ->
+        [seq j <- arrivals_between arr_seq t1 t2 | job_arrival j < t] = [::].
+    Proof.
+      move=> t1 t2 t LT.
+      case: (leqP t1 t2) => RANGE;
+        last by rewrite /arrivals_between big_geq //=; lia.
+      rewrite filter_in_pred0 // => j IN.
+      rewrite -ltnNge.
+      apply: (ltn_trans LT).
+      rewrite ltnS.
+      by apply: job_arrival_between_ge; eauto.
+    Qed.
+
+    (** Furthermore, if we filter the list of arrivals in an interval
+        <<[t1,t2)>> with an arrival-time threshold less than [t2],
+        we can simply discard the tail past the threshold. *)
+    Lemma arrivals_between_filter :
+      forall t1 t2 t,
+        t <= t2 ->
+        arrivals_between arr_seq t1 t
+        = [seq j <- arrivals_between arr_seq t1 t2 | job_arrival j < t].
+    Proof.
+      move=> t1 t2 t LE2.
+      case: (leqP t1 t2) => RANGE;
+        last by rewrite /arrivals_between !big_geq //=; lia.
+      case: (leqP t1 t) => LE1;
+        last by rewrite [LHS]/arrivals_between big_geq; try lia; rewrite arrivals_between_filter_nil.
+      rewrite /arrivals_between bigcat_nat_filter_eq_filter_bigcat_nat.
+      rewrite (big_cat_nat _ _ _ LE1 LE2) //=.
+      rewrite !big_nat [X in _ ++ X]big1; last first.
+      { move=> t' /andP[LO HI].
+        rewrite filter_in_pred0 // => j IN.
+        have -> : job_arrival j = t' by apply: job_arrival_at; eauto.
+        rewrite -leqNgt.
+        exact: LO. }
+      { rewrite cats0.
+        apply: eq_bigr => t' /andP[LO HI].
+        apply esym.
+        apply /all_filterP/allP => j IN.
+        have -> : job_arrival j = t' by apply: job_arrival_at; eauto.
+        exact: HI. }
+    Qed.
+
+    (** Next, we prove that if a job belongs to the prefix
+        (jobs_arrived_before t), then it arrives in the arrival
+        sequence. *)
+    Lemma in_arrivals_implies_arrived:
+      forall j t1 t2,
+        j \in arrivals_between arr_seq t1 t2 ->
+        arrives_in arr_seq j.
+    Proof. by move=> ? ? ? /mem_bigcat_nat_exists[arr [? _]]; exists arr. Qed.
+
+    (** We also prove a weaker version of the above lemma. *)
+    Lemma in_arrseq_implies_arrives:
+      forall t j,
+        j \in arr_seq t ->
+        arrives_in arr_seq j.
+    Proof. by move=> t ? ?; exists t. Qed.
+
+    (** Next, we prove that if a job belongs to the prefix
+         (jobs_arrived_between t1 t2), then it indeed arrives between t1 and
+         t2. *)
+    Lemma in_arrivals_implies_arrived_between:
+      forall j t1 t2,
+        j \in arrivals_between arr_seq t1 t2 ->
+        arrived_between j t1 t2.
+    Proof. by move=> ? ? ? /mem_bigcat_nat_exists[t0 [/job_arrival_at <-]]. Qed.
+
+    (** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
+           then it indeed arrives before time t. *)
+    Lemma in_arrivals_implies_arrived_before:
+      forall j t,
+        j \in arrivals_before arr_seq t ->
+        arrived_before j t.
+    Proof. by move=> ? ? /in_arrivals_implies_arrived_between. Qed.
+
+    (** Similarly, we prove that if a job from the arrival sequence arrives
+        before t, then it belongs to the sequence (jobs_arrived_before t). *)
+    Lemma arrived_between_implies_in_arrivals:
+      forall j t1 t2,
+        arrives_in arr_seq j ->
+        arrived_between j t1 t2 ->
+        j \in arrivals_between arr_seq t1 t2.
+    Proof.
+      move=> j t1 t2 [a_j arrj] before; apply: mem_bigcat_nat (arrj).
+      by rewrite -(job_arrival_at arrj).
+    Qed.
+
+    (** Any job in arrivals between time instants [t1] and [t2] must arrive
+       in the interval <<[t1,t2)>>. *)
+    Lemma job_arrival_between_P:
+      forall j P t1 t2,
+        j \in arrivals_between_P arr_seq P t1 t2 ->
+        t1 <= job_arrival j < t2.
+    Proof.
+      move=> j P t1 t2.
+      rewrite mem_filter => /andP[Pj /mem_bigcat_nat_exists[i [+ iitv]]].
+      by move=> /job_arrival_at ->.
+    Qed.
+
+    (** Any job [j] is in the sequence [arrivals_between t1 t2] given
+     that [j] arrives in the interval <<[t1,t2)>>. *)
+    Lemma job_in_arrivals_between:
+      forall j t1 t2,
+        arrives_in arr_seq j ->
+        t1 <= job_arrival j ->
+        job_arrival j < t2 ->
+        j \in arrivals_between arr_seq t1 t2.
+    Proof.
+      move=> j t1 t2 ARRSEQ ARR1 ARR2; apply: mem_bigcat_nat.
+      - by apply /andP; split; [exact ARR1| exact ARR2].
+      - by apply job_in_arrivals_at => //=.
+    Qed.
+
+    (** Next, we prove that if the arrival sequence doesn't contain duplicate
+        jobs, the same applies for any of its prefixes. *)
+    Lemma arrivals_uniq:
+      arrival_sequence_uniq arr_seq ->
+      forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
+    Proof.
+      move=> SET t1 t2; apply: bigcat_nat_uniq => // j t1' t2'.
+      by move=> /job_arrival_at <- /job_arrival_at <-.
+    Qed.
+
+    (** Also note that there can't by any arrivals in an empty time interval. *)
+    Lemma arrivals_between_geq:
+      forall t1 t2,
+        t1 >= t2 ->
+        arrivals_between arr_seq t1 t2  = [::].
+    Proof. by move=> ? ? ?; rewrite /arrivals_between big_geq. Qed.
+
+    (** Conversely, if a job arrives, the considered interval is non-empty. *)
+    Corollary arrivals_between_nonempty :
+      forall t1 t2 j,
+        j \in arrivals_between arr_seq t1 t2 -> t1 < t2.
+    Proof. by move=> j1 j2 t; apply: contraPltn=> LEQ; rewrite arrivals_between_geq. Qed.
+
+    (** Given jobs [j1] and [j2] in [arrivals_between_P arr_seq P t1 t2], the fact that
+        [j2] arrives strictly before [j1] implies that [j2] also belongs in the sequence
+        [arrivals_between_P arr_seq P t1 (job_arrival j1)]. *)
+    Lemma arrival_lt_implies_job_in_arrivals_between_P :
+      forall (j1 j2 : Job) (P : Job -> bool) (t1 t2 : instant),
+        j1 \in arrivals_between_P arr_seq P t1 t2 ->
+        j2 \in arrivals_between_P arr_seq P t1 t2 ->
+        job_arrival j2 < job_arrival j1 ->
+        j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1).
+    Proof.
+      move=> j1 j2 P t1 t2.
+      rewrite !mem_filter => /andP[_ j1arr] /andP[Pj2 j2arr] arr_lt.
+      rewrite Pj2/=; apply: job_in_arrivals_between => //=.
+      - exact: in_arrivals_implies_arrived j2arr.
+      - by rewrite (job_arrival_between_ge j2arr).
+    Qed.
+
+    (** For ease of rewriting, we establish the equivalence between a job's membership in
+        [arrivals_between] and its membership in [arrives_in], subject to constraints on
+        the job's arrival time. *)
+    Lemma job_arrival_in_bounds :
+      forall (j : Job) (t1 t2 : instant),
+        (j \in arrivals_between arr_seq t1 t2)
+        <-> (arrives_in arr_seq j /\ t1 <= job_arrival j < t2).
+    Proof.
+      move => j t1 t2; split.
+      - move => IN; split.
+        + by eapply in_arrivals_implies_arrived => //=.
+        + by apply in_arrivals_implies_arrived_between in IN => //=.
+      - move => [IN ARR].
+        by apply arrived_between_implies_in_arrivals => //=.
+    Qed.
+
+    (** We observe that, by construction, the sequence of arrivals is
+        sorted by arrival times. To this end, we first define the
+        order relation. *)
+    Definition by_arrival_times (j1 j2 : Job) : bool := job_arrival j1 <= job_arrival j2.
+
+    (** Trivially, the arrivals at any one point in time are ordered
+        w.r.t. arrival times. *)
+    Lemma arrivals_at_sorted :
+      forall t,
+        sorted by_arrival_times (arrivals_at arr_seq t).
+    Proof.
+      move=> t.
+      have AT_t : forall j, j \in (arrivals_at arr_seq t) -> job_arrival j = t
+        by move=> j; apply job_arrival_at.
+      case: (arrivals_at arr_seq t) AT_t => // j' js AT_t.
+      apply /(pathP j') => i LT.
+      rewrite /by_arrival_times !AT_t //;
+        last by apply mem_nth; auto.
+      rewrite in_cons; apply /orP; right.
+      by exact: mem_nth.
+   Qed.
+
+    (** By design, the list of arrivals in any interval is sorted. *)
+    Lemma arrivals_between_sorted :
+      forall t1 t2,
+        sorted by_arrival_times (arrivals_between arr_seq t1 t2).
+    Proof.
+      move=> t1 t2.
+      rewrite /arrivals_between.
+      elim: t2 => [|t2 SORTED];
+        first by rewrite big_nil.
+      case: (leqP t1 t2) => T1T2;
+        last by rewrite big_geq.
+      rewrite (big_cat_nat _ _ _ T1T2 _) //=.
+      case A1: (\cat_(t1<=t<t2)arrivals_at arr_seq t) => [|j js];
+        first by rewrite cat0s big_nat1; exact: arrivals_at_sorted.
+      have CAT : path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i).
+      { rewrite cat_path; apply /andP; split.
+        { move: SORTED. rewrite /sorted A1 => PATH_js.
+          by rewrite /path -/(path _ _ js) /by_arrival_times; apply /andP; split. }
+        { rewrite big_nat1.
+          case A2: (arrivals_at arr_seq t2) => // [j' js'].
+          apply path_le with (x' := j').
+          { by rewrite /transitive/by_arrival_times; lia. }
+          { rewrite /by_arrival_times.
+            have -> : job_arrival j' = t2
+              by apply job_arrival_at; rewrite A2; apply mem_head.
+            set L := (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)).
+            have EX : exists t', L \in arrivals_at arr_seq t' /\ t1 <= t' < t2
+              by apply mem_bigcat_nat_exists; rewrite /L A1 last_cons; exact: mem_last.
+            move: EX => [t' [IN /andP [t1t' t't2]]].
+            have -> : job_arrival L = t' by apply job_arrival_at.
+            by lia. }
+          { move: (arrivals_at_sorted t2); rewrite /sorted A2 => PATH'.
+            rewrite /path -/(path _ _ js') {1}/by_arrival_times.
+            by apply /andP; split => //. } } }
+      by move: CAT; rewrite /sorted A1 cat_cons {1}/path -/(path _ _ (js ++ _)) => /andP [_ CAT].
+   Qed.
+
+  End ArrivalTimes.
+
+  (** In the following section, we establish a lemma that allows splitting the arrival sequence by task. *)
+  Section ArrivalPartition.
+
+    (** If all jobs stem from tasks in a given task set [ts]... *)
+    Variable ts : seq Task.
+    Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+    (** ... then we can partition the arrival sequence by task. *)
+    Lemma arrivals_between_partitioned_by_task:
+      forall t1 t2 j,
+        (j \in arrivals_between arr_seq t1 t2)
+        = (j \in \cat_(tsk <- ts) task_arrivals_between arr_seq tsk t1 t2).
+    Proof.
+      move=> t1 t2 j.
+      rewrite /task_arrivals_between.
+      set l:= arrivals_between arr_seq t1 t2.
+      rewrite -{1}(@filter_predT _ l).
+      under eq_big_seq.
+      { move=> tsk tsk_IN.
+        rewrite (@eq_in_filter _ _ (fun j => (predT j) && (job_of_task tsk j))) => //.
+        over. }
+      apply bigcat_partitions => j' IN' pred_true.
+      apply H_all_jobs_from_taskset.
+      by apply in_arrivals_implies_arrived in IN'.
+    Qed.
+
+  End ArrivalPartition.
+
+End ArrivalSequencePrefix.
+
+(** In this section, we establish a few auxiliary facts about the
+    relation between the property of being scheduled and arrival
+    predicates to facilitate automation. *)
+Section ScheduledImpliesArrives.
+
+  (** Consider any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+
+  (** Consider any kind of processor state model, ... *)
+  Context {PState : ProcessorState Job}.
+
+  (** ... any job arrival sequence with consistent arrivals, .... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times 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. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+
+  (** Next, consider a job [j] ... *)
+  Variable j : Job.
+
+  (** ... which is scheduled at a time instant [t]. *)
+  Variable t : instant.
+  Hypothesis H_scheduled_at : scheduled_at sched j t.
+
+  (** Then we show that [j] arrives in [arr_seq]. *)
+  Lemma arrives_in_jobs_come_from_arrival_sequence :
+    arrives_in arr_seq j.
+  Proof.
+    by apply: H_jobs_come_from_arrival_sequence H_scheduled_at.
+  Qed.
+
+  (** Job [j] has arrived by time instant [t]. *)
+  Lemma arrived_between_jobs_must_arrive_to_execute :
+    has_arrived j t.
+  Proof.
+    by apply: H_jobs_must_arrive_to_execute H_scheduled_at.
+  Qed.
+
+  (** For any future time [t'], job [j] arrives before [t']. *)
+  Lemma arrivals_before_scheduled_at :
+    forall t',
+      t < t' ->
+      j \in arrivals_before arr_seq t'.
+  Proof.
+    move=> t' LTtt'.
+    apply: arrived_between_implies_in_arrivals => //.
+    apply: leq_ltn_trans LTtt'.
+    by apply: arrived_between_jobs_must_arrive_to_execute.
+  Qed.
+
+  (** Similarly, job [j] arrives up to time [t'] for any [t'] such that [t <= t']. *)
+  Lemma arrivals_up_to_scheduled_at :
+    forall t',
+      t <= t' ->
+      j \in arrivals_up_to arr_seq t'.
+  Proof.
+    by move=> t' LEtt'; apply arrivals_before_scheduled_at; lia.
+  Qed.
+
+End ScheduledImpliesArrives.
+
+(** 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
+       any_ready_job_is_pending
+       arrivals_before_scheduled_at
+       arrivals_uniq
+       arrived_between_implies_in_arrivals
+       arrived_between_jobs_must_arrive_to_execute
+       arrives_in_jobs_come_from_arrival_sequence
+       backlogged_implies_arrived
+       job_scheduled_implies_ready
+       jobs_must_arrive_to_be_ready
+       jobs_must_arrive_to_be_ready
+       ready_implies_arrived
+       valid_schedule_implies_jobs_must_arrive_to_execute
+       valid_schedule_jobs_come_from_arrival_sequence
+       valid_schedule_jobs_must_be_ready_to_execute
+       uniq_valid_arrival
+       consistent_times_valid_arrival
+       job_arrival_arrives_at
+       job_in_arrivals_between
+  : basic_rt_facts.

restructuring/analysis/basic_facts/completion.v → analysis/facts/behavior/completion.v

-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.service.
-Require Export rt.restructuring.analysis.basic_facts.arrivals.
+Require Export prosa.analysis.facts.behavior.service.
+Require Export prosa.analysis.facts.behavior.arrivals.
+Require Export prosa.analysis.definitions.schedule_prefix.
+Require Export prosa.analysis.definitions.job_properties.
 
-Require Export rt.util.nat.
+(** * Completion *)
 
 (** In this file, we establish basic facts about job completions. *)
-
 Section CompletionFacts.
+
   (** Consider any job type,...*)
   Context {Job: JobType}.
   Context `{JobCost Job}.
+  Context `{JobArrival Job}.
 
   (** ...any kind of processor model,... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...and a given schedule. *)
   Variable sched: schedule PState.
 
-  (** Let j be any job that is to be scheduled. *)
+  (** Let [j] be any job that is to be scheduled. *)
   Variable j: Job.
 
-  (** We prove that after job j completes, it remains completed. *)
+  (** We prove that after job [j] completes, it remains completed. *)
   Lemma completion_monotonic:
     forall t t',
       t <= t' ->
       completed_by sched j t ->
       completed_by sched j t'.
-  Proof.
-    move => t t' LE. rewrite /completed_by /service => COMP.
-    apply leq_trans with (n := service_during sched j 0 t); auto.
-      by apply service_monotonic.
-  Qed.
+  Proof. move=> ? ? ? /leq_trans; apply; exact: service_monotonic. Qed.
+
+  (** We prove that if [j] is not completed by [t'], then it's also not
+      completed by any earlier instant. *)
+  Lemma incompletion_monotonic:
+    forall t t',
+      t <= t' ->
+      ~~ completed_by sched j t' ->
+      ~~ completed_by sched j t.
+  Proof. move=> ? ? ?; exact/contra/completion_monotonic. Qed.
 
   (** We observe that being incomplete is the same as not having received
      sufficient service yet... *)
   Lemma less_service_than_cost_is_incomplete:
     forall t,
       service sched j t < job_cost j
-      <->
-      ~~ completed_by sched j t.
-  Proof.
-    move=> t. by split; rewrite /completed_by; [rewrite -ltnNge // | rewrite ltnNge //].
-  Qed.
+      <-> ~~ completed_by sched j t.
+  Proof. by move=> ?; rewrite -ltnNge. Qed.
 
   (** ...which is also the same as having positive remaining cost. *)
   Lemma incomplete_is_positive_remaining_cost:
     forall t,
       ~~ completed_by sched j t
-      <->
-      remaining_cost sched j t > 0.
+      <-> remaining_cost sched j t > 0.
   Proof.
-    move=> t. by split; rewrite /remaining_cost -less_service_than_cost_is_incomplete subn_gt0 //.
+    by move=> ?; rewrite -less_service_than_cost_is_incomplete subn_gt0.
   Qed.
 
-  (** Assume that completed jobs do not execute. *)
-  Hypothesis H_completed_jobs:
-    completed_jobs_dont_execute sched.
+  (** Trivially, it follows that an incomplete job has a positive cost. *)
+  Corollary incomplete_implies_positive_cost:
+    forall t,
+      ~~ completed_by sched j t ->
+      job_cost_positive j.
+  Proof.
+    move=> t INCOMP; apply: leq_trans (leq_subr (service sched j t) _).
+    by rewrite -incomplete_is_positive_remaining_cost.
+  Qed.
+
+  (** In the remainder of this section, we assume that schedules are
+      "well-formed": jobs are scheduled neither before their arrival
+      nor after their completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs : completed_jobs_dont_execute sched.
+
+  (** Clearly, if a job is scheduled, its cost is positive. *)
+  Lemma scheduled_implies_positive_cost :
+    forall t,
+      scheduled_at sched j t ->
+      0 < job_cost j.
+  Proof.
+    move=> t SCHED; move_neq_up ZE; move: ZE.
+    by rewrite leqn0 => /eqP ZE; apply H_completed_jobs in SCHED; rewrite ZE in SCHED.
+  Qed.
+
+  (** To simplify subsequent proofs, we restate the assumption
+      [H_completed_jobs] as a trivial corollary. *)
+  Corollary service_lt_cost :
+    forall t,
+      scheduled_at sched j t -> service sched j t < job_cost j.
+  Proof. exact: H_completed_jobs. Qed.
+
+  (** We observe that a job that is completed at the instant of its
+      arrival has a cost of zero. *)
+  Lemma completed_on_arrival_implies_zero_cost :
+    completed_by sched j (job_arrival j) ->
+    job_cost j = 0.
+  Proof.
+    by rewrite /completed_by no_service_before_arrival// leqn0 => /eqP.
+  Qed.
 
   (** Further, we note that if a job receives service at some time t, then its
-     remaining cost at this time is positive. *)
+      remaining cost at this time is positive. *)
   Lemma serviced_implies_positive_remaining_cost:
     forall t,
       service_at sched j t > 0 ->
       remaining_cost sched j t > 0.
   Proof.
     move=> t SERVICE.
-    rewrite -incomplete_is_positive_remaining_cost -less_service_than_cost_is_incomplete.
-    apply H_completed_jobs.
-    by apply service_at_implies_scheduled_at.
+    rewrite -incomplete_is_positive_remaining_cost.
+    rewrite -less_service_than_cost_is_incomplete.
+    exact/service_lt_cost/service_at_implies_scheduled_at.
   Qed.
 
   (** Consequently, if we have a have processor model where scheduled jobs
@@ -78,56 +118,59 @@ Section CompletionFacts.
   (** Assume a scheduled job always receives some positive service. *)
   Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
 
+  (** To simplify subsequent proofs, we restate the assumption
+      [H_scheduled_implies_serviced] as a trivial corollary. *)
+  Corollary scheduled_implies_serviced :
+    forall s,
+      scheduled_in j s -> 0 < service_in j s.
+  Proof. exact: H_scheduled_implies_serviced. Qed.
+
   (** Then a scheduled job has positive remaining cost. *)
   Corollary scheduled_implies_positive_remaining_cost:
     forall t,
       scheduled_at sched j t ->
       remaining_cost sched j t > 0.
   Proof.
-    rewrite /scheduled_at => t SCHEDULED.
-      by apply: serviced_implies_positive_remaining_cost; rewrite /service_at; apply: H_scheduled_implies_serviced.
+    move=> t sch.
+    exact/serviced_implies_positive_remaining_cost/scheduled_implies_serviced.
   Qed.
 
-  (** We also prove that a completed job cannot be scheduled... *)
-  Lemma completed_implies_not_scheduled:
+  (** We also prove that a scheduled job cannot be completed... *)
+  Lemma scheduled_implies_not_completed :
     forall t,
-      completed_by sched j t ->
-      ~~ scheduled_at sched j t.
+      scheduled_at sched j t -> ~~ completed_by sched j t.
   Proof.
-    move=> t COMP.
-    apply contra with (b := ~~ completed_by sched j t);
-      last by apply /negPn.
-    move=> SCHED. move: (H_completed_jobs j t SCHED).
-    by rewrite less_service_than_cost_is_incomplete.
+    move=> t sch.
+    by rewrite -less_service_than_cost_is_incomplete service_lt_cost.
   Qed.
 
-  (** ... and that a scheduled job cannot be completed. *)
-  Lemma scheduled_implies_not_completed:
+  (** ... and that a completed job cannot be scheduled. *)
+  Lemma completed_implies_not_scheduled :
     forall t,
-      scheduled_at sched j t ->
-      ~~ completed_by sched j t.
+      completed_by sched j t -> ~~ scheduled_at sched j t.
+  Proof. move=> ? /negPn; exact/contra/scheduled_implies_not_completed. Qed.
+
+  (** Job [j] cannot be pending before and at time [0]. *)
+  Remark not_pending_earlier_and_at_0 :
+    ~~ pending_earlier_and_at sched j 0.
   Proof.
-    move=> t SCHED.
-    have REMPOS := scheduled_implies_positive_remaining_cost t SCHED.
-    rewrite /remaining_cost subn_gt0 in REMPOS.
-      by rewrite -less_service_than_cost_is_incomplete.
+    rewrite /pending_earlier_and_at negb_and; apply/orP; left.
+    by rewrite /arrived_before -ltnNge.
   Qed.
 
 End CompletionFacts.
 
-
+(** In this section, we establish some facts that are really about service,
+    but are also related to completion and rely on some of the above lemmas.
+    Hence they are in this file rather than in the service facts file. *)
 Section ServiceAndCompletionFacts.
-  (** In this section, we establish some facts that are really about service,
-      but are also related to completion and rely on some of the above lemmas.
-      Hence they are in this file rather than in the service facts file. *)
 
   (** Consider any job type,...*)
   Context {Job: JobType}.
   Context `{JobCost Job}.
 
   (** ...any kind of processor model,... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...and a given schedule. *)
   Variable sched: schedule PState.
@@ -136,12 +179,19 @@ Section ServiceAndCompletionFacts.
   Hypothesis H_completed_jobs:
     completed_jobs_dont_execute sched.
 
-  (** Let j be any job that is to be scheduled. *)
+  (** Let [j] be any job that is to be scheduled. *)
   Variable j: Job.
 
   (** Assume that a scheduled job receives exactly one time unit of service. *)
   Hypothesis H_unit_service: unit_service_proc_model PState.
 
+  (** To simplify subsequent proofs, we restate the assumption
+      [H_unit_service] as a trivial corollary. *)
+  Lemma unit_service :
+    forall s,
+      service_in j s <= 1.
+  Proof. exact: H_unit_service. Qed.
+
   (** To begin with, we establish that the cumulative service never exceeds a
      job's total cost if service increases only by one at each step since
      completed jobs don't execute. *)
@@ -149,18 +199,15 @@ Section ServiceAndCompletionFacts.
     forall t,
       service sched j t <= job_cost j.
   Proof.
-    move=> t.
-    elim: t => [|t]; first by rewrite service0.
+    elim=> [|t]; first by rewrite service0.
     rewrite -service_last_plus_before.
-    rewrite leq_eqVlt => /orP [/eqP EQ|LT].
-    - rewrite not_scheduled_implies_no_service;
-        first by rewrite addn0 EQ.
-      apply completed_implies_not_scheduled => //.
+    rewrite leq_eqVlt => /orP[/eqP EQ|LT].
+    - rewrite not_scheduled_implies_no_service ?EQ ?addn0//.
+      apply: completed_implies_not_scheduled => //.
       by rewrite /completed_by EQ.
-    - apply leq_trans with (n := service sched j t + 1);
-        last by rewrite addn1.
-      rewrite leq_add2l.
-      by apply H_unit_service.
+    - have: service_at sched j t <= 1 by exact: unit_service.
+      rewrite -(leq_add2l (service sched j t)) => /leq_trans; apply.
+      by rewrite addn1.
   Qed.
 
   (** This lets us conclude that [service] and [remaining_cost] are complements
@@ -168,40 +215,35 @@ Section ServiceAndCompletionFacts.
   Lemma service_cost_invariant:
     forall t,
       (service sched j t) + (remaining_cost sched j t) = job_cost j.
-  Proof.
-    move=> t.
-    rewrite /remaining_cost subnKC //.
-    by apply service_at_most_cost.
-  Qed.
+  Proof. by move=> ?; rewrite subnKC// service_at_most_cost. Qed.
 
-  (** We show that the service received by job j in any interval is no larger
+  (** We show that the service received by job [j] in any interval is no larger
      than its cost. *)
   Lemma cumulative_service_le_job_cost:
     forall t t',
       service_during sched j t t' <= job_cost j.
   Proof.
     move=> t t'.
-    case/orP: (leq_total t t') => [tt'|tt']; last by rewrite service_during_geq //.
-    apply leq_trans with (n := service sched j t'); last by apply: service_at_most_cost.
-    rewrite /service. rewrite -(service_during_cat sched j 0 t t') // leq_addl //.
+    have [t'_le_t|t_lt_t'] := leqP t' t; first by rewrite service_during_geq.
+    apply: leq_trans (service_at_most_cost t').
+    by rewrite -(service_cat _ _ _ _ (ltnW t_lt_t')) leq_addl.
   Qed.
 
-  (** If a job isn't complete at time t, it can't be completed at time (t +
-     remaining_cost j t - 1). *)
+  (** If a job isn't complete at time [t], it can't be completed at time [t +
+     remaining_cost j t - 1]. *)
   Lemma job_doesnt_complete_before_remaining_cost:
     forall t,
       ~~ completed_by sched j t ->
       ~~ completed_by sched j (t + remaining_cost sched j t - 1).
   Proof.
-    move=> t.
-    rewrite incomplete_is_positive_remaining_cost => REMCOST.
+    move=> t; rewrite incomplete_is_positive_remaining_cost => rem_cost.
     rewrite -less_service_than_cost_is_incomplete -(service_cat sched j t);
-    last by rewrite -addnBA //; apply: leq_addr.
-    apply leq_ltn_trans with (n := service sched j t + remaining_cost sched j t - 1).
-    - by rewrite -!addnBA //; rewrite leq_add2l; apply cumulative_service_le_delta; exact.
-    - rewrite service_cost_invariant // -subn_gt0 subKn //.
-      move: REMCOST. rewrite /remaining_cost subn_gt0 => SERVICE.
-        by apply leq_ltn_trans with (n := service sched j t).
+      last by rewrite -addnBA//; exact: leq_addr.
+    have: service sched j t + remaining_cost sched j t - 1 < job_cost j.
+    { rewrite service_cost_invariant -subn_gt0 subKn//.
+      exact/(leq_trans rem_cost)/leq_subr. }
+    apply: leq_ltn_trans.
+    by rewrite -!addnBA// leq_add2l cumulative_service_le_delta.
   Qed.
 
   Section GuaranteedService.
@@ -213,26 +255,30 @@ Section ServiceAndCompletionFacts.
     Context `{JobArrival Job}.
     Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched.
 
+    (** To simplify subsequent proofs, we restate the assumption
+        [H_jobs_must_arrive] as a trivial corollary. *)
+    Corollary has_arrived_scheduled :
+      forall t,
+        scheduled_at sched j t -> has_arrived j t.
+    Proof. exact: H_jobs_must_arrive. Qed.
+
     (** We show that if job j is scheduled, then it must be pending. *)
     Lemma scheduled_implies_pending:
       forall t,
         scheduled_at sched j t ->
         pending sched j t.
     Proof.
-      move=> t SCHED.
-      rewrite /pending.
-      apply /andP; split;
-        first by apply: H_jobs_must_arrive => //.
-      by apply: scheduled_implies_not_completed => //.
+      move=> t sch; apply/andP; split; first exact: has_arrived_scheduled.
+      exact: scheduled_implies_not_completed.
     Qed.
 
   End GuaranteedService.
 
 End ServiceAndCompletionFacts.
 
+(** In this section, we establish facts that on jobs with non-zero costs that
+    must arrive to execute. *)
 Section PositiveCost.
-  (** In this section, we establish facts that on jobs with non-zero costs that
-      must arrive to execute. *)
 
   (** Consider any type of jobs with cost and arrival-time attributes,...*)
   Context {Job: JobType}.
@@ -240,17 +286,16 @@ Section PositiveCost.
   Context `{JobArrival Job}.
 
   (** ...any kind of processor model,... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...and a given schedule. *)
   Variable sched: schedule PState.
 
-  (** Let j be any job that is to be scheduled. *)
+  (** Let [j] be any job that is to be scheduled. *)
   Variable j: Job.
 
-  (** We assume that job j has positive cost, from which we can
-     infer that there always is a time in which j is pending, ... *)
+  (** We assume that job [j] has positive cost, from which we can
+     infer that there always is a time in which [j] is pending, ... *)
   Hypothesis H_positive_cost: job_cost j > 0.
 
   (** ...and that jobs must arrive to execute. *)
@@ -266,29 +311,25 @@ Section PositiveCost.
         job_arrival j <= t' < t
         /\ scheduled_at sched j t'.
   Proof.
-    rewrite /completed_by.
-    move=> t COMPLETE.
-    have POSITIVE_SERVICE: 0 < service sched j t
-      by apply leq_trans with (n := job_cost j); auto.
-      by apply: positive_service_implies_scheduled_since_arrival; assumption.
+    move=> t comp.
+    have: 0 < service sched j t by exact: leq_trans comp.
+    exact: positive_service_implies_scheduled_since_arrival.
   Qed.
 
   (** We also prove that the job is pending at the moment of its arrival. *)
   Lemma job_pending_at_arrival:
     pending sched j (job_arrival j).
   Proof.
-    rewrite /pending.
-    apply/andP; split;
-    first by rewrite /has_arrived //.
-    rewrite /completed_by no_service_before_arrival // -ltnNge //.
+    apply/andP; split; first by rewrite /has_arrived.
+    by rewrite /completed_by no_service_before_arrival// -ltnNge.
   Qed.
 
 End PositiveCost.
 
 Section CompletedJobs.
+
   (** Consider any kinds of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.
 
   (** Consider any schedule... *)
   Variable sched : schedule PState.
@@ -297,29 +338,29 @@ Section CompletedJobs.
      readiness. *)
   Context `{JobCost Job}.
   Context `{JobArrival Job}.
-  Context `{JobReady Job PState}.
+  Context {jr : JobReady Job PState}.
 
   (** We observe that a given job is ready only if it is also incomplete... *)
   Lemma ready_implies_incomplete:
     forall j t, job_ready sched j t -> ~~ completed_by sched j t.
-  Proof.
-    move=> j t READY.
-    move: (any_ready_job_is_pending sched j t READY).
-    by rewrite /pending => /andP [_ INCOMPLETE].
-  Qed.
+  Proof. by move=> ? ? /any_ready_job_is_pending /andP[]. Qed.
 
   (** ...and lift this observation also to the level of whole schedules. *)
   Lemma completed_jobs_are_not_ready:
     jobs_must_be_ready_to_execute sched ->
     completed_jobs_dont_execute sched.
   Proof.
-    rewrite /jobs_must_be_ready_to_execute /completed_jobs_dont_execute.
-    move=> READY_IF_SCHED j t SCHED.
-    move: (READY_IF_SCHED j t SCHED) => READY.
-    rewrite less_service_than_cost_is_incomplete.
-    by apply ready_implies_incomplete.
+    move=> + j t sch => /(_ j t sch) ready.
+    by rewrite less_service_than_cost_is_incomplete ready_implies_incomplete.
   Qed.
 
+  (** Furthermore, in a valid schedule, completed jobs don't execute. *)
+  Corollary valid_schedule_implies_completed_jobs_dont_execute:
+    forall arr_seq, 
+    valid_schedule sched arr_seq ->
+    completed_jobs_dont_execute sched.
+  Proof. move=> ? [? ?]; exact: completed_jobs_are_not_ready. Qed.
+
   (** We further observe that completed jobs don't execute if scheduled jobs
      always receive non-zero service and cumulative service never exceeds job
      costs. *)
@@ -329,11 +370,46 @@ Section CompletedJobs.
     completed_jobs_dont_execute sched.
   Proof.
     move=> IDEAL SERVICE_BOUND j t SCHED.
-    have UB := SERVICE_BOUND j t.+1.
-    have POS := IDEAL _ _ SCHED.
-    apply ltn_leq_trans with (n := service sched j t.+1) => //.
-    rewrite -service_last_plus_before /service_at.
-    by rewrite -{1}(addn0 (service sched j t)) ltn_add2l.
+    apply: leq_trans (SERVICE_BOUND j t.+1).
+    by rewrite -service_last_plus_before -addn1 leq_add2l IDEAL.
   Qed.
 
 End CompletedJobs.
+
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
+    will be able to apply it automatically. *)
+Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_rt_facts.
+
+(** Next, we relate the completion of jobs in schedules with identical prefixes. *)
+Section CompletionInTwoSchedules.
+  (** Consider any processor model and any type of jobs with costs, arrival times, and a notion of readiness. *)
+  Context {Job: JobType} {PState: ProcessorState Job}.
+  Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.
+
+  (** If two schedules share a common prefix, then (in the prefix) jobs
+      complete in one schedule iff they complete in the other. *)
+  Lemma identical_prefix_completed_by:
+    forall sched1 sched2 h,
+      identical_prefix sched1 sched2 h ->
+      forall j t,
+        t <= h ->
+        completed_by sched1 j t = completed_by sched2 j t.
+  Proof.
+    move=> sched1 sched2 h PREFIX j t LE_h.
+    rewrite /completed_by (identical_prefix_service sched1 sched2)//.
+    exact: identical_prefix_inclusion PREFIX.
+  Qed.
+
+  (** For convenience, we restate the previous lemma in terms of [pending]. *)
+  Corollary identical_prefix_pending:
+    forall sched1 sched2 h,
+      identical_prefix sched1 sched2 h ->
+      forall j t,
+        t <= h ->
+        pending sched1 j t = pending sched2 j t.
+  Proof.
+    move=> sched1 sched2 h PREFIX j t t_le_h.
+    by rewrite /pending (identical_prefix_completed_by _ sched2 h).
+  Qed.
+
+End CompletionInTwoSchedules.

restructuring/analysis/basic_facts/deadlines.v → analysis/facts/behavior/deadlines.v

-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.service.
-Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export prosa.analysis.facts.behavior.completion.
+
+(** * Deadlines *)
 
 (** In this file, we observe basic properties of the behavioral job
     model w.r.t. deadlines. *)
-
 Section DeadlineFacts.
+
   (** Consider any given type of jobs with costs and deadlines... *)
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
+
   (** ... any given type of processor states. *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
+
+  (** First, we derive two properties from the fact that a job is incomplete at
+      some point in time. *)
+  Section Incompletion.
+
+    (** Consider any given schedule. *)
+    Variable sched: schedule PState.
+
+    (** Trivially, a job that both meets its deadline and is incomplete at a
+        time [t] must have a deadline later than [t]. *)
+    Lemma incomplete_implies_later_deadline:
+      forall j t,
+        job_meets_deadline sched j ->
+        ~~ completed_by sched j t ->
+        t < job_deadline j.
+    Proof.
+      move=> j t MET INCOMP; apply: contraT; rewrite -leqNgt => PAST_DL.
+      have /negP// : ~~ completed_by sched j (job_deadline j).
+      exact: incompletion_monotonic INCOMP.
+    Qed.
+
+    (** Furthermore, a job that both meets its deadline and is incomplete at a
+        time [t] must be scheduled at some point between [t] and its
+        deadline. *)
+    Lemma incomplete_implies_scheduled_later:
+      forall j t,
+        job_meets_deadline sched j ->
+        ~~ completed_by sched j t ->
+        exists t', t <= t' < job_deadline j /\ scheduled_at sched j t'.
+    Proof.
+      move=> j t MET INCOMP.
+      apply: cumulative_service_implies_scheduled.
+      rewrite -(ltn_add2l (service sched j t)) addn0.
+      rewrite service_cat; last exact/ltnW/incomplete_implies_later_deadline.
+      by apply: leq_trans MET; rewrite less_service_than_cost_is_incomplete.
+    Qed.
 
-  (** We begin with schedules / processor models in which scheduled jobs
-    always receive service. *)
+  End Incompletion.
+
+  (** Next, we look at schedules / processor models in which scheduled jobs
+      always receive service. *)
   Section IdealProgressSchedules.
 
     (** Consider a given reference schedule... *)
@@ -25,26 +63,19 @@ Section DeadlineFacts.
     (** ...and scheduled jobs always receive service. *)
     Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
 
-    (** We observe that, if a job is known to meet its deadline, then
-       its deadline must be later than any point at which it is
-       scheduled. That is, if a job that meets its deadline is
-       scheduled at time t, we may conclude that its deadline is at a
-       time later than t. *)
+    (** We observe that if a job meets its deadline and is scheduled at time
+        [t], then then its deadline is at a time later than t. *)
     Lemma scheduled_at_implies_later_deadline:
       forall j t,
         job_meets_deadline sched j ->
         scheduled_at sched j t ->
         t < job_deadline j.
     Proof.
-      move=> j t.
-      rewrite /job_meets_deadline => COMP SCHED.
-      case: (boolP (t < job_deadline j)) => //.
-      rewrite -leqNgt => AFTER_DL.
-      apply completion_monotonic with (t' := t) in COMP => //.
-      apply scheduled_implies_not_completed in SCHED => //.
-      move/negP in SCHED. contradiction.
+      move=> j t MET SCHED_AT.
+      apply: (incomplete_implies_later_deadline sched) => //.
+      exact: scheduled_implies_not_completed.
     Qed.
-    
+
   End IdealProgressSchedules.
 
   (** In the following section, we observe that it is sufficient to
@@ -65,8 +96,7 @@ Section DeadlineFacts.
         (job_meets_deadline sched j <-> job_meets_deadline sched' j).
     Proof.
       move=> j SERVICE.
-      split;
-        by rewrite /job_meets_deadline /completed_by -SERVICE.
+      by split; rewrite /job_meets_deadline /completed_by -SERVICE.
     Qed.
 
   End EqualProgress.