interference_bound_edf.v

                rewrite leq_add2r; unfold a_fst, a_lst, j_fst, j_lst.
                rewrite -[num_mid_jobs.+1]add0n; apply prev_le_next;
                  last by rewrite add0n H_at_least_two_jobs ltnSn.
                by ins; apply interference_bound_edf_jobs_ordered_by_arrival.
              }
              by rewrite big_const_nat iter_addn mul1n addn0.
            Qed.
            
            (* ... which results in proving that (a_lst + D_k) - t1 <= D_i.
               This holds because high-priority jobs have earlier deadlines. Therefore,
               the interference caused by the first job is bounded by D_i %% p_k - (D_k - R_k). *)
            Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :
              interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k).
            Proof.
              apply interference_bound_edf_simpl_by_moving_to_left_side.
              apply (leq_trans interference_bound_edf_bounding_interference_with_interval_lengths).
              rewrite interference_bound_edf_simpl_by_concatenation_of_intervals leq_subLR.
              have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
              destruct LST as [_ [ LSTserv _]].
              unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
                                                  -interference_bound_edf_j_i_deadline.
              by apply interference_under_edf_implies_shorter_deadlines in LSTserv.
            Qed.

          End InterferenceOfFirstJob.

          (* Using the lemmas above we show that the interference bound works in the
             case of two or more jobs. *)
          Lemma interference_bound_edf_holds_for_multiple_jobs :
            \sum_(0 <= i < num_mid_jobs.+2)
              interference_caused_by (nth elem sorted_jobs i) t1 t2 <= interference_bound.
          Proof.
            (* Knowing that we have at least two elements, we take first and last out of the sum *) 
            rewrite [nth]lock big_nat_recl // big_nat_recr // /= -lock.
            rewrite addnA addnC addnA.

            have NK := interference_bound_edf_n_k_equals_num_mid_jobs_plus_one. 

            (* We use the lemmas we proved to show that the interference bound holds. *)
            unfold interference_bound, edf_specific_interference_bound.
            fold D_i D_k p_k n_k.
            rewrite addnC addnA; apply leq_add;
              first by rewrite addnC interference_bound_edf_holds_for_middle_and_last_jobs.
            rewrite leq_min; apply/andP; split.
            {
              apply interference_bound_edf_interference_le_task_cost.
              rewrite interference_bound_edf_job_in_same_sequence.
              by apply mem_nth; rewrite H_at_least_two_jobs.
            }
            by apply interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack.
          Qed.
          
        End InterferenceTwoOrMoreJobs.

      End InterferenceManyJobs.
      
      Theorem interference_bound_edf_bounds_interference :
        x <= interference_bound.
      Proof.
        (* Use the definition of workload based on list of jobs. *)
        rewrite interference_bound_edf_use_another_definition. 

        (* We only care about the jobs that cause interference. *)
        rewrite interference_bound_edf_simpl_by_filtering_interfering_jobs.

        (* Now we order the list by job arrival time. *)
        rewrite interference_bound_edf_simpl_by_sorting_interfering_jobs.

        (* Next, we show that the workload bound holds if n_k
           is no larger than the number of interferings jobs. *)
        destruct (size sorted_jobs <= n_k) eqn:NUM;
          first by apply interference_bound_edf_holds_for_at_most_n_k_jobs.
        apply negbT in NUM; rewrite -ltnNge in NUM.

        (* Find some dummy element to use in the nth function *)
        assert (EX: exists elem: JobIn arr_seq, True).
          destruct sorted_jobs as [| j]; [by rewrite ltn0 in NUM | by exists j].
        destruct EX as [elem _].

        (* Now we index the sum to access the first and last elements. *)
        rewrite (big_nth elem).

        (* First, we show that the bound holds for an empty list of jobs. *)
        destruct (size sorted_jobs) as [| n] eqn:SIZE;
          first by rewrite big_geq.

        (* Then, we show the same for a single job, or for multiple jobs. *)
        rewrite SIZE; destruct n as [| num_mid_jobs].
        {
          rewrite big_nat_recr // big_geq //.
          rewrite [nth]lock /= -lock add0n.
          by apply interference_bound_edf_holds_for_a_single_job; rewrite SIZE.
        }
        {
          by apply interference_bound_edf_holds_for_multiple_jobs; first by rewrite SIZE.
        }
      Qed.
      
    End MainProof.
    
  End ProofInterferenceBound.

End EDFSpecificBound.