Library rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_service

Require Import rt.util.all.
Require Import rt.model.priority rt.model.suspension.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task
               rt.model.arrival.basic.task_arrival
               rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.arrival.jitter.job.
Require Import rt.model.schedule.uni.schedulability rt.model.schedule.uni.service
               rt.model.schedule.uni.workload
               rt.model.schedule.uni.response_time.
Require Import rt.model.schedule.uni.jitter.schedule
               rt.model.schedule.uni.jitter.platform.
Require Import rt.model.schedule.uni.susp.suspension_intervals
               rt.model.schedule.uni.susp.schedule
               rt.model.schedule.uni.susp.platform
               rt.model.schedule.uni.susp.valid_schedule.
Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule
               rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties.
Require Import rt.model.schedule.uni.transformation.construction.

(* In this file, we compare the service received by the analyzed job j after
   reducing the suspension-aware schedule to a jitter-aware schedule. *)
Module JitterScheduleService.

  Import Job SporadicTaskset Suspension Priority SuspensionIntervals Workload Service
         UniprocessorScheduleWithJitter Schedulability ResponseTime TaskArrival
         ScheduleConstruction ValidSuspensionAwareSchedule.

  Module basic := schedule.UniprocessorSchedule.
  Module susp := ScheduleWithSuspensions.
  Module jitter_aware := Platform.
  Module susp_aware := PlatformWithSuspensions.
  Module job_jitter := JobWithJitter.
  Module reduction := JitterScheduleConstruction.
  Module reduction_prop := JitterScheduleProperties.

  (* We begin by providing the initial setup and definitions in Sections 1 to 5.
     The main results are proven later in Sections 6-(A) to 6-(C). *)
  Section ProvingScheduleProperties.

    Context {Task: eqType}.
    Variable task_cost: Task → time.
    Variable task_period: Task → time.
    Variable task_deadline: Task → time.
    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_cost: Job → time.
    Variable job_deadline: Job → time.
    Variable job_task: Job → Task.

    (* Let ts be any task set. *)
    Variable ts: seq Task.

    (* Next, consider any consistent, duplicate-free job arrival sequence... *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent:
      arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.

    (* ...where all jobs come from task set ts. *)
    Hypothesis H_jobs_from_taskset:
      ∀ j, arrives_in arr_seq j → job_task j \in ts.

    (* Since we consider real-time tasks, assume that job deadlines are equal to task deadlines. *)
    Hypothesis H_job_deadlines_equal_task_deadlines:
      ∀ j, arrives_in arr_seq j → job_deadline j = task_deadline (job_task j).

    (* Also assume that tasks have constrained deadlines and that jobs arrive sporadically.
       (Note: this is required to bound the interference of previous jobs of the analyzed task.) *)
    Hypothesis H_constrained_deadlines:
      constrained_deadline_model task_period task_deadline ts.
    Hypothesis H_sporadic_arrivals:
      sporadic_task_model task_period job_arrival job_task arr_seq.

    (* Consider any FP policy that is reflexive, transitive and total. *)
    Variable higher_eq_priority: FP_policy Task.
    Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
    Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
    Let job_higher_eq_priority := FP_to_JLDP job_task higher_eq_priority.

    (* Assume that jobs have associated suspension times. *)
    Variable job_suspension_duration: job_suspension Job.

    (* Next, consider any valid suspension-aware schedule of this arrival sequence.
       (Note: see definition in rt.model.schedule.uni.susp.valid_schedule.v) *)
    Variable sched_susp: schedule Job.
    Hypothesis H_valid_schedule:
      valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
                                      job_suspension_duration job_cost sched_susp.

    (* Finally, recall the notion of job response-time bound and deadline miss in sched_susp. *)
    Let job_response_time_in_sched_susp_bounded_by :=
      is_response_time_bound_of_job job_arrival job_cost sched_susp.
    Let job_misses_no_deadline_in_sched_susp :=
      job_misses_no_deadline job_arrival job_cost job_deadline sched_susp.

    (* Recall that we are going to analyze the response time of some job after
       applying the reduction to the jitter-aware schedule as defined in
       rt.analysis.uni.susp.dynamic.jitter.jitter_schedule. *)

    (* Let j be the job to be analyzed. *)
    Variable j: Job.
    Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
    Let arr_j := job_arrival j.

    (* Let R_j be any value that we want to prove to be a response-time bound for job j in sched_susp.
       Note that in the context of this proof, R_j also delimits the length of the schedules
       that we are going to analyze, i.e., we only care about the interval [0, arr_j + R_j). *)
    Variable R_j: time.

    (* Next, recall the definition of higher-or-equal-priority tasks (other than j's task). *)
    Let other_hep_task tsk_other :=
      higher_eq_priority tsk_other (job_task j) && (tsk_other != job_task j).

    (* Assume that each job of a higher-or-equal-priority task (other than j's task) is
       associated a response-time bound R_hp.
       (Note: this follows from analyzing the higher-priority tasks in a previous step.) *)
    Variable R_hp: Job → time.
    Hypothesis H_bounded_response_time_of_hp_jobs:
      ∀ j_hp,
        arrives_in arr_seq j_hp →
        other_hep_task (job_task j_hp) →
        job_response_time_in_sched_susp_bounded_by j_hp (R_hp j_hp).

    (* Also assume that all the previous jobs of same task as j do not miss any
       deadlines in sched_susp.
       (Note: this is an induction hypothesis that is easily obtained when analyzing the
        sequence of jobs of the same task.) *)
    Hypothesis H_no_deadline_misses_for_previous_jobs:
      ∀ j0,
        arrives_in arr_seq j0 →
        job_arrival j0 < job_arrival j →
        job_task j0 = job_task j →
        job_misses_no_deadline_in_sched_susp j0.

    (* Having stated all the properties of the suspension-aware schedule, now we recall
       the construction of the jitter-aware schedule and the corresponding job parameters. *)
    Let sched_jitter := reduction.sched_jitter job_arrival job_task arr_seq higher_eq_priority
                                               job_cost job_suspension_duration j R_hp.
    Let inflated_job_cost := reduction.inflated_job_cost job_cost job_suspension_duration j.
    Let job_jitter := reduction.job_jitter job_arrival job_task higher_eq_priority job_cost j R_hp.

    (* By the end of this file, we are going to show that if job j completes by time (arr_j + R_j)
       in sched_jitter, then it also completes by time (arr_j + R_j) in sched_susp.
       The argument is based on the fact that the service of higher-or-equal-priority jobs is moved
       from the interval [0, arr_j) to the interval [arr_j, arr_j + R_j), when we introduce jitter.
       
       The proofs are structured in the three final sections. In Section 6-A, we prove that
       sched_jitter provides provides less service for higher-or-equal-priority jobs during [0, arr_j).
       In Section B, we prove that sched_jitter provides more service for higher-or-equal-priority
       jobs during [arr_j, arr_j + R). In Section 6-C, we conclude with the main theorem that compares
       the response time of job j in both schedules. *)

    (* For simplicity, let's define some local names... *)
    Let actual_job_arrival := actual_arrival job_arrival job_jitter.
    Let job_arrived_before := arrived_before job_arrival.
    Let job_has_arrived := has_arrived job_arrival.
    Let job_has_actually_arrived := jitter_has_passed job_arrival job_jitter.
    Let job_completed_in_sched_jitter := completed_by inflated_job_cost sched_jitter.

    (* ...and also recall definitions related to the suspension-aware schedule. *)
    Let job_suspended_at :=
      suspended_at job_arrival job_cost job_suspension_duration sched_susp.
    Let job_cumulative_suspension :=
      cumulative_suspension_during job_arrival job_cost job_suspension_duration sched_susp.
    Let job_completed_in_sched_susp := completed_by job_cost sched_susp.
    Let backlogged_in_sched_susp := susp.backlogged job_arrival job_cost
                                                    job_suspension_duration sched_susp.

    (* Since we'll have to reason about sets of arriving jobs with and without jitter,
       let's use simpler names for those as well. *)
    Let arrivals := jobs_arrived_between arr_seq.
    Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.

    (* Because we are dealing with a bounded scheduling window, we also identify all
       job arrivals (with and without jitter) in the interval [0, arr_j + R_j). *)
    Let arrivals_before_end_of_interval := arrivals 0 (arr_j + R_j).
    Let actual_arrivals_before_end_of_interval := actual_arrivals 0 (arr_j + R_j).

    (* Next, by checking jobs priorities, ... *)
    Let other_higher_eq_priority_job j_hp :=
      higher_eq_priority (job_task j_hp) (job_task j) && (j_hp != j).

    (* ...we identify the workload of higher-or-equal-priority jobs (other than j)
       that arrive in any interval [t1, t2), in the original schedule,... *)
    Definition workload_of_other_hep_jobs_in_sched_susp t1 t2 :=
      workload_of_jobs job_cost (arrivals t1 t2) other_higher_eq_priority_job.

    (* ... and also the workload of higher-or-equal priority jobs (other than j)
       with actual arrival time in the interval [t1, t2), in the jitter-aware schedule. *)
    Definition workload_of_other_hep_jobs_in_sched_jitter t1 t2 :=
      workload_of_jobs inflated_job_cost (actual_arrivals t1 t2) other_higher_eq_priority_job.

    (* Next, we recall the cumulative service of all higher-or-equal-priority
       jobs (other than j) that arrived in the interval [0, arr_j + R_j),
       received in a given interval [t1, t2) in the original schedule. *)
    Definition service_of_other_hep_jobs_in_sched_susp t1 t2 :=
      service_of_jobs sched_susp arrivals_before_end_of_interval other_higher_eq_priority_job t1 t2.

    (* Similarly, we recall the cumulative service of all higher-or-equal-priority
       jobs (other than j) with actual arrival time in the interval [0, arr_j + R_j),
       received in a given interval [t1, t2) in the jitter-aware schedule. *)
    Definition service_of_other_hep_jobs_in_sched_jitter t1 t2 :=
      service_of_jobs sched_jitter actual_arrivals_before_end_of_interval
                      other_higher_eq_priority_job t1 t2.

    (* Before moving to the main results, let's prove some auxiliary lemmas about service/workload. *)
    Section AuxiliaryLemmas.

      (* First, we prove that if all higher-or-equal-priority jobs have completed by
         some time t in the jitter-aware schedule, then the service received
         by those jobs up to time t amounts to the requested workload. *)
      Section ServiceEqualsWorkload.

        (* Let t be any time no later than (arr_j + R_j)... *)
        Variable t: time.
        Hypothesis H_before_end_of_interval: t ≤ arr_j + R_j.

        (* ...in which all higher-or-equal-priority jobs (other than j) have completed. *)
        Hypothesis H_workload_has_finished:
          ∀ j_hp,
            arrives_in arr_seq j_hp →
            actual_arrival_before job_arrival job_jitter j_hp t →
            other_higher_eq_priority_job j_hp →
            job_completed_in_sched_jitter j_hp t.

        (* Then, the service received by all those jobs in the interval [0, t) amounts to
           the workload requested by them in the interval [0, t). *)
        Lemma jitter_reduction_service_equals_workload_in_jitter:
          service_of_other_hep_jobs_in_sched_jitter 0 t ≥
          workload_of_other_hep_jobs_in_sched_jitter 0 t.

      End ServiceEqualsWorkload.

      (* Next, we prove a lemma showing that service in the suspension-aware schedule
         is bounded by the workload. *)
      Section ServiceBoundedByWorkload.

        (* Consider any time t <= arr_j + R_j. *)
        Variable t: time.
        Hypothesis H_before_end_of_interval: t ≤ arr_j + R_j.

        (* Then, the service of all jobs with higher-or-equal-priority that arrive in
           the interval [0, arr_j + R_j), received in the interval [0, t), is no
           larger than the workload of all jobs with higher-or-equal-priority that
           are released in the interval [0, t), in the suspension-aware schedule. *)
        Lemma jitter_reduction_service_in_sched_susp_le_workload:
          service_of_other_hep_jobs_in_sched_susp 0 t ≤
          workload_of_other_hep_jobs_in_sched_susp 0 t.

      End ServiceBoundedByWorkload.

    End AuxiliaryLemmas.

    (* In this section we prove that before the arrival of job j, the cumulative service
       received by other higher-or-equal-priority is no larger in the jitter-aware schedule
       than in the suspension-aware schedule. *)
    Section LessServiceBeforeArrival.

      (* In fact, we can prove that the service is not larger for each higher-or-equal-priority
         job in isolation. *)
      Section LessServiceForEachJob.

          (* Let j_hp be any higher-or-equal-priority job (different from j). *)
          Variable j_hp: Job.
          Hypothesis H_arrives: arrives_in arr_seq j_hp.
          Hypothesis H_higher_or_equal_priority: other_higher_eq_priority_job j_hp.

          (* For simplicity, let's define some local names. *)
          Let arr_hp := job_arrival j_hp.
          Let cost_hp := job_cost j_hp.
          Let Rhp := R_hp j_hp.

          (* Using a series of case analyses, we are going to prove that
               service sched_jitter j_hp t <= service sched_susp j_hp t. *)
          Section Case1.

            (* Case 1. Assume that j_hp is a job from the same task as j. *)
            Hypothesis H_same_task: job_task j_hp = job_task j.

            (* Due to constrained deadlines, we can infer that previous jobs of the same task
               complete in sched_susp before j arrives. Because these jobs do not have inflated
               costs, they cannot receive more service in sched_jitter before the arrival of j. *)
            Lemma jitter_reduction_less_job_service_before_interval_case1:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case1.

          Section Case2.

            (* Case 2. Assume that j_hp is a job from another task,... *)
            Hypothesis H_different_task: job_task j_hp != job_task j.

            (* ...that is released (with jitter) no earlier than the arrival of j. *)
            Hypothesis H_released_no_earlier: arr_j ≤ actual_job_arrival j_hp.

            (* Since j_hp cannot execute in sched_jitter, the claim trivially holds. *)
            Lemma jitter_reduction_less_job_service_before_interval_case2:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case2.

          Section Case3.

            (* Case 3. Assume that j_hp is a job from another task,... *)
            Hypothesis H_different_task: job_task j_hp != job_task j.

            (* ...and that (arr_j - arr_hp < arr_j - cost_hp). *)
            Hypothesis H_distance_is_smaller:
              arr_j - arr_hp < Rhp - cost_hp.

            (* By definition, the jitter of j_hp is set so that it arrives after j.
               Since j_hp cannot execute in sched_jitter, the claim follows trivially. *)
            Lemma jitter_reduction_less_job_service_before_interval_case3:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case3.

          Section Case4.

            (* Case 4. Assume that j_hp is a job from another task... *)
            Hypothesis H_different_task: job_task j_hp != job_task j.

            (* ...and that j_hp completes in sched_susp before j arrives. *)
            Hypothesis H_completes_before_j_arrives: arr_hp + Rhp ≤ arr_j.

            (* Since j_hp completes early in sched_susp and receives maximum service, it cannot
               receive more service in sched_jitter before j arrives, thus the claim holds. *)
            Lemma jitter_reduction_less_job_service_before_interval_case4:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case4.

          Section Case5.

            (* Case 5. Assume that j_hp is a job from another task,... *)
            Hypothesis H_different_task: job_task j_hp != job_task j.

            (* ...that is released (with jitter) before the arrival of j. *)
            Hypothesis H_released_before: actual_job_arrival j_hp < arr_j.

            (* Also assume that (arr_j < arr_hp + Rhp) and (Rhp - costhp <= arr_j - arr_hp). *)
            Hypothesis H_j_hp_completes_after_j_arrives: arr_j < arr_hp + Rhp.
            Hypothesis H_distance_is_not_smaller: Rhp - cost_hp ≤ arr_j - arr_hp.

            (* Note that in this case the jitter of job j_hp is set to (Rhp - cost_hp). *)
            Remark jitter_reduction_jitter_equals_R_minus_cost:
              job_jitter j_hp = Rhp - cost_hp.

            (* Since j_hp is released late in sched_jitter with "slack" (Rhp - cost_hp), even
               if it executes at full speed, it cannot beat sched_susp in terms of service.
               Therefore, the claim also holds. *)
            Lemma jitter_reduction_less_job_service_before_interval_case5:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case5.

          (* Using the case analysis above, we conclude that before the arrival of job j,
             any higher-or-equal-priority job receives no more service in the jitter-aware
             schedule than in the suspension-aware schedule. *)
          Lemma jitter_reduction_less_job_service_before_interval:
            service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

      End LessServiceForEachJob.

      (* Since the result about service applies to each individual job, we can prove that
         it also holds for the cumulative service of all higher-or-equal-priority jobs. *)
      Corollary jitter_reduction_less_service_before_the_interval:
        service_of_other_hep_jobs_in_sched_jitter 0 arr_j ≤
        service_of_other_hep_jobs_in_sched_susp 0 arr_j.

    End LessServiceBeforeArrival.

    (* So far, we have shown that the higher-or-equal-priority jobs receives less service
       in the jitter-aware schedule during [0, arr_j). Recall that our final goal is to show
       that all this service is actually moved into the interval [arr_j, arr_j + R_j) and
       converted into interference for the job j being analyzed.
       In this section, we reason about what happens to high-priority jobs after job j arrives. *)
    Section MoreServiceAfterArrival.

      (* First, we show that the workload is conserved at every point in the interval
         [arr_j, arr_j + R_j). *)
      Section Conservation.

        (* Consider any time t >= arr_j (no earlier than the arrival of j). *)
        Variable t: time.
        Hypothesis H_no_earlier_than_j: t ≥ arr_j.

        (* Then, we prove that every job that arrives up to time t is also released
           in the jitter-aware schedule up to time t. *)
        Lemma jitter_reduction_actual_arrival_before_end_of_interval:
          ∀ j_hp,
            other_higher_eq_priority_job j_hp →
            job_arrival j_hp ≤ t →
            actual_job_arrival j_hp ≤ t.

        (* This implies that the workload is conserved up to time t (inclusive). That is,
           in the jitter-aware schedule, there's always as much (high-priority) work to be
           executed as in the original schedule. *)
        Lemma jitter_reduction_workload_conservation_inside_interval:
            workload_of_other_hep_jobs_in_sched_susp 0 t.+1 ≤
            workload_of_other_hep_jobs_in_sched_jitter 0 t.+1.

      End Conservation.

      (* Since the higher-or-equal-priority jobs receive no more service in the jitter-aware
         schedule during [0, arr_j), and because the workload is conserved, we prove next
         that those jobs receive no less service in the jitter-aware schedule in the interval
         [arr_j, arr_j + R_j).  *)
      Section MoreServiceInsideTheInterval.

        (* The claim we need to show is presented next. The proof follows by induction on
           the interval length d:
             forall d,
               d <= R_j ->
               service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) <= 
               service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d).    *)

        (* Since the base case of the induction is trivial, we focus on the inductive step. *)
        Section InductiveStep.

          (* By strong induction, assume that for a given interval length d < R_j, ... *)
          Variable d: time.
          Hypothesis H_d_lt_R: d < R_j.

          (* ...the higher-or-equal-priority jobs (other than j) received as much service in
             the jitter-aware schedule during [arr_j, arr_j + d) as in the suspension-aware
             schedule. *)
          Hypothesis H_induction_hypothesis:
            service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) ≤
            service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d).

          (* Now we must prove that the claim continues to hold for interval [arr_j, arr_j + d + 1):

              service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) <=
              service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1). *)

          (* The proof begins with a case analysis on whether there are pending
             higher-or-equal-priority jobs at time (arr_j + d) in the jitter-aware schedule. *)
          Section NoPendingJobs.

            (* Case 1. Assume that all higher-or-equal-priority jobs (other than j) whose jitter
                       has passed by time (arr_j + d) are already complete at time (arr_j + d)
                       in the jitter-aware schedule. *)
            Hypothesis H_all_jobs_completed_in_sched_jitter:
              ∀ j_hp,
                arrives_in arr_seq j_hp →
                other_higher_eq_priority_job j_hp →
                job_has_actually_arrived j_hp (arr_j + d) →
                job_completed_in_sched_jitter j_hp (arr_j + d).

            (* First, we show that the service received in the suspension-aware schedule
               during [arr_j, arr_j + d + 1) is bounded by the difference between the
               requested workload and the service received prior to the arrival of job j. *)
            Lemma jitter_reduction_convert_service_to_workload:
              service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) ≤
                workload_of_other_hep_jobs_in_sched_susp 0 (arr_j + d + 1)
                - service_of_other_hep_jobs_in_sched_susp 0 arr_j.

            (* Because of workload conservation, we show that the workload in the suspension-aware
               schedule is bounded by the workload in the jitter-aware schedule. *)
            Lemma jitter_reduction_compare_workload:
                  workload_of_other_hep_jobs_in_sched_susp 0 (arr_j + d + 1)
                          - service_of_other_hep_jobs_in_sched_susp 0 arr_j
               ≤ workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
                          - service_of_other_hep_jobs_in_sched_susp 0 arr_j.

            (* Since the higher-or-equal-priority jobs received less service in the
               jitter-aware schedule in the interval [0, arr_j), we can compare the
               service in the two schedules. *)
            Lemma jitter_reduction_compare_service:
                  workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
                          - service_of_other_hep_jobs_in_sched_susp 0 arr_j
               ≤ workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
                         - service_of_other_hep_jobs_in_sched_jitter 0 arr_j.

            (* Having inferred that the difference between the workload and service is that
               large in the jitter-aware schedule, we can convert this difference back to
               service received in the interval [arr_j, arr_j + d + 1] in sched_jitter. *)
            Lemma jitter_reduction_convert_workload_to_service:
              workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1) -
                service_of_other_hep_jobs_in_sched_jitter 0 arr_j ≤
              service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).

            (* By combining each inequality above in sequence, we complete the induction
               step for Case 1. *)
            Lemma jitter_reduction_inductive_step_case1:
                service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) ≤
                service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).

          End NoPendingJobs.

          Section ThereArePendingJobs.

            (* Case 2. Assume that there are higher-or-equal-priority jobs (other than j) whose
                       jitter has passed by time (arr_j + d) that are still pending at time
                       (arr_j + d) in the jitter-aware schedule. *)
            Hypothesis H_there_are_pending_jobs_in_sched_jitter:
              ∃ j_hp,
                arrives_in arr_seq j_hp ∧
                other_higher_eq_priority_job j_hp ∧
                job_has_actually_arrived j_hp (arr_j + d) ∧
                ~~ job_completed_in_sched_jitter j_hp (arr_j + d).

            (* By the induction hypothesis, the higher-or-equal-priority jobs received
               as much service in the jitter-aware schedule as in the suspension-aware
               schedule in the interval [arr_j, arr_j + d). Therefore, it only remains
               to show that:

               service_of_other_hep_jobs_in_sched_susp (arr_j + d) (arr_j + d + 1) <=
               service_of_other_hep_jobs_in_sched_jitter (arr_j + d) (arr_j + d + 1). *)

            (* Because the LHS in the inequality above cannot be larger than 1 (single point),
               it suffices to show that there is a higher-or-equal-priority job (different from j)
               scheduled at time (arr_j + d) in the jitter-aware schedule. That follows
               from two facts:
               (a) The jitter-aware schedule is work-conserving and enforces priorities.
                   Therefore, even if the job j_hp in the hypothesis above is not scheduled,
                   there will always be a job with higher-or-equal-priority being scheduled. 
               (b) If there is at least one higher-or-equal-priority pending job, by the
                   additional property we embedded in the schedule construction, we avoid
                   scheduling job j (see lemma sched_jitter_does_not_pick_j). *)
            Lemma jitter_reduction_inductive_step_case2:
              service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) ≤
              service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).

          End ThereArePendingJobs.

        End InductiveStep.

        (* Using the proof by induction above, we conclude that, for any interval length
           d <= R_j, the service received by higher-or-equal-priority jobs (other than j)
           in the interval [arr_j, arr_j + d) in the jitter-aware schedule is as large as
           the corresponding service in the suspension-aware schedule. *)
        Lemma jitter_reduction_more_service_inside_the_interval:
          ∀ d,
            d ≤ R_j →
            service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) ≤
            service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d).

      End MoreServiceInsideTheInterval.

    End MoreServiceAfterArrival.

    (* In this section, we prove that the generated schedule is "worse" for job j.
       More precisely, job j receives no more service in the jitter-aware schedule
       than the cumulative service and suspension time in the original schedule. *)
    Section JitterAwareScheduleIsWorse.

      (* Recall the definition of job response-time bound in sched_jitter. *)
      Let job_response_time_in_sched_jitter_bounded_by :=
        is_response_time_bound_of_job job_arrival inflated_job_cost sched_jitter.

      (* From this point, we are going to analyze both schedules up to time (arr_j + R_j) and
         compare the service received by job j. At the end, we are going to prove that R_j is
         also a response-time bound for job j in the suspension-aware schedule sched_susp. *)

      (* First, we show that the service received by job j in the interval [arr_j, arr_j + R_j)
         is always bounded by the difference between the interval length R_j and the service
         received by the other higher-or-equal-priority jobs in the same interval. *)
      Lemma jitter_reduction_service_jitter:
        service_during sched_jitter j arr_j (arr_j + R_j) ≤
        R_j - service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + R_j).

      (* Next, since we want to infer that job j is schedulable in the suspension-aware
         schedule if it is schedulable in the jitter-aware schedule, we can assume by
         contrapositive that job j has not completed by time (arr_j + R_j) in
         the suspension-aware schedule. *)
      Section JobNotCompleted.

        (* Assume that j has not completed by (arr_j + R_j) in the suspension-aware schedule. *)
        Hypothesis H_j_not_completed:
          ~~ job_completed_in_sched_susp j (arr_j + R_j).

        (* Then, we can prove that the difference between the interval length and
           the service received by the other higher-or-equal-priority jobs during
           [arr_j, arr_j + R_j) in the suspension-aware schedule is bounded by
           the cumulative service and suspension time of job j. *)
        Lemma jitter_reduction_service_susp:
          R_j - service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + R_j) ≤
          service_during sched_susp j arr_j (arr_j + R_j) +
          job_cumulative_suspension j arr_j (arr_j + R_j).

        (* Since the higher-or-equal-priority jobs receive more service during
           [arr_j, arr_j + R_j) in the jitter-aware schedule and produce more
           interference, it follows that job j cannot receive as much service
           in the jitter-aware schedule as in the suspension-aware schedule. *)
        Lemma jitter_reduction_less_service_for_job_j:
          service_during sched_jitter j arr_j (arr_j + R_j) ≤
          service_during sched_susp j arr_j (arr_j + R_j)
          + job_cumulative_suspension j arr_j (arr_j + R_j).

      End JobNotCompleted.

      (* Suppose that the response time of job j is bounded by R_j in sched_jitter. *)
      Hypothesis H_response_time_of_j_in_sched_jitter:
        job_response_time_in_sched_jitter_bounded_by j R_j.

      (* Then, using the lemmas above, we conclude that the response time of job j in sched_susp
         is also bounded by R_j. *)
      Corollary jitter_reduction_job_j_completes_no_later:
        job_response_time_in_sched_susp_bounded_by j R_j.

    End JitterAwareScheduleIsWorse.

  End ProvingScheduleProperties.

End JitterScheduleService.