Kimaya Bedarkar
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
          rewrite (eq_big (fun j=> pred_task (job_task j)) job_cost) //;
            last by move=> j'; rewrite /pred_task; move: TSK => /eqP ->.
          erewrite (eq_big pred_task); [|by done|by move=> tsk'; eauto].
-          by apply: sum_of_jobs_le_sum_rbf; eauto. } }
+          by apply: sum_of_jobs_le_sum_rbf; eauto. }
+        by unfold quiet_time; move: BUSY => [[_ [T1 T2]] _].
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
      (** ... and assume that the schedule is idle at [t]. *)
      Hypothesis H_idle : is_idle sched t.

-      (** We prove that in this case: ... *)
-
-      (** ... interference from higher-or-equal priority jobs from
-          another task is equal to [false], ... *)
-      Lemma idle_implies_no_hep_task_interference :
-        forall j, is_interference_from_hep_job_from_another_task j t = false.
-      Proof.
-        intros j.
-        unfold is_interference_from_hep_job_from_another_task.
-        by move: (H_idle) => /eqP ->.
-      Qed.
-
+      (* can be potentially moved, if [task_interference_received_before] is moved *)
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
          erewrite service_of_jobs_case_on_pred with (P2 := fun j' => j' != j); rt_eauto.
          erewrite workload_of_jobs_case_on_pred with (P' := fun j' => j' != j); rt_eauto.
          replace ((fun j0 : Job => hep_job j0 j && (j0 != j))) with (another_hep_job^~j); last by rewrite /another_hep_job.
-          rewrite -/(service_of_other_hep_jobs j 0 t) -cumulative_i_ohep_eq_service_of_ohep; eauto.
+          rewrite /service_of_jobs.
+          rewrite -cumulative_pred_eq_service; rt_eauto.
+          replace (\sum_(j0 <- arrivals_between arr_seq 0 t | hep_job j0 j && ~~ (j0 != j))
+     service_during sched j0 0 t) with ( service_of_jobs sched (fun j0 : Job => hep_job j0 j && ~~ (j0 != j))
+    (arrivals_between arr_seq 0 t) 0 t).
--- a/analysis/definitions/interference.v 0 → 100644
+++ b/analysis/definitions/interference.v 0 → 100644
+
+  (** ... where jobs do not execute before their arrival nor after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Consider a JLFP-policy that indicates a higher-or-equal priority relation,
+     and assume that this relation is reflexive and transitive. *)
+  Context `{JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  Hypothesis H_priority_is_transitive : transitive_priorities.
+
+(** Next, we say that job [j] is incurring interference from another
+      job with higher or equal priority at time [t], if there exists a
+      job [jhp] (different from [j]) with higher or equal priority
+      that executes at time [t]. *)
+  Definition is_interference_from_another_hep_job (j : Job) (t : instant) :=