remove redundant clause from `busy_intervals_are_bounded_by`

Busy intervals by definition always include the job arrival time, so
stating `t1 <= job_arrival j < t2` explicitly is not required.

Closes: #93

analysis/abstract/abstract_rta.v

@@ -439,7 +439,7 @@ Section Abstract_RTA.
           specialize (L1 H0).
           feed_n 2 L1; try done.
           { move: (H_busy_interval_exists j H_j_arrives H_job_of_tsk H_job_cost_positive)
-            => [t1' [t2' [_ [BOUND BUSY]]]].
+            => [t1' [t2' [BOUND BUSY]]].
             have EQ:= busy_interval_is_unique _ _ _ _ _ _ _ _ H_busy_interval BUSY.
             destruct EQ as [EQ1 EQ2].
             subst t1' t2'; clear BUSY.
@@ -467,7 +467,7 @@ Section Abstract_RTA.
         Lemma relative_arrival_is_bounded: A < L.
         Proof.
           rewrite /A.
-          move: (H_busy_interval_exists j H_j_arrives H_job_of_tsk H_job_cost_positive) => [t1' [t2' [_ [BOUND BUSY]]]].
+          move: (H_busy_interval_exists j H_j_arrives H_job_of_tsk H_job_cost_positive) => [t1' [t2' [BOUND BUSY]]].
           have EQ:= busy_interval_is_unique _ _ _ _ _ _ _ _ H_busy_interval BUSY. destruct EQ as [EQ1 EQ2].
           subst t1' t2'; clear BUSY.
           apply leq_trans with (t2 - t1); last by rewrite leq_subLR.
@@ -535,8 +535,8 @@ Section Abstract_RTA.
     intros j ARR JOBtsk. unfold job_response_time_bound.
     move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
     { by rewrite /completed_by ZERO. } 
-    move: (H_busy_interval_exists j ARR JOBtsk POS) => [t1 [t2 [NEQ [T2 BUSY]]]].
-    move: (NEQ) (BUSY)=> /andP [GE LT] [_ QTt2].
+    move: (H_busy_interval_exists j ARR JOBtsk POS) => [t1 [t2 [T2 BUSY]]].
+    move: (BUSY) => [[/andP [GE LT] _] QTt2].
     have A2LTL := relative_arrival_is_bounded _ ARR JOBtsk POS _ _ BUSY.
     set (A2 := job_arrival j - t1) in *.
     move: (representative_exists tsk _ interference_bound_function _ A2LTL) => [A1 [ALEA2 [EQΦ INSP]]].

analysis/abstract/definitions.v

@@ -175,7 +175,6 @@ Section AbstractRTADefinitions.
           job_of_task tsk j ->
           job_cost j > 0 ->
           exists t1 t2,
-            t1 <= job_arrival j < t2 /\
             t2 <= t1 + L /\
             busy_interval j t1 t2.
 

results/edf/rta/bounded_pi.v

@@ -292,7 +292,6 @@ Section AbstractRTAforEDFwithArrivalCurves.
         with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
       { by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
       exists t1, t2; split; first by done.
-      split; first by done.
       by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
     Qed.
     

results/fifo/rta.v

@@ -199,7 +199,6 @@ Section AbstractRTAforFIFOwithArrivalCurves.
         with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
       { by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
       { exists t1, t2; split; first by done.
-        split; first by done.
         by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto. }
     Qed.
 

results/fixed_priority/rta/bounded_pi.v

@@ -242,7 +242,6 @@ Section AbstractRTAforFPwithArrivalCurves.
         rt_eauto.
       { by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_hep_rbf. }
       exists t1, t2; split; first by done.
-      split; first by done.
       by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
     Qed.