Finish EDF instantiation of abstract RTA

model/schedule/uni/limited/edf/nonpr_reg/fixed/response_time_bound.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job
+               rt.model.arrival.basic.task_arrival
+               rt.model.priority.
+Require Import rt.model.schedule.uni.service
+               rt.model.schedule.uni.workload
+               rt.model.schedule.uni.schedule
+               rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.limited.schedule
+               rt.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound
+               rt.model.schedule.uni.limited.rbf.
+Require Import rt.model.arrival.curves.bounds. 
+Require Import rt.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.model.schedule.uni.limited.platform.limited.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+ 
+(** * RTA for EDF-schedulers with fixed premption points *)
+(** In this module we prove a general RTA theorem for EDF-schedulers with fixed preemption points *)
+Module RTAforFixedPreemptionPointsModelwithArrivalCurves.
+
+  Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+         ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
+         RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
+  
+  Section Analysis.
+
+    Context {Task: eqType}.
+    Variable task_cost: Task -> time.
+    Variable task_deadline: Task -> time.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+
+    (* For clarity, let's denote the relative deadline of a task as D. *)
+    Let D tsk := task_deadline tsk.
+
+    (* The deadline of a job is equal to the deadline of the corresponding task. *)
+    Let job_deadline j := D (job_task j).
+
+    (* Consider the EDF policy that indicates a higher-or-equal priority relation. *)
+    Let higher_eq_priority: JLFP_policy Job := EDF job_arrival job_deadline.
+
+    (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+    (* Consider an arbitrary task set ts. *)
+    Variable ts: list Task.
+
+    (* Assume that all jobs come from the task set... *)
+    Hypothesis H_all_jobs_from_taskset:
+      forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+    (* ...and the cost of a job cannot be larger than the task cost. *)
+    Hypothesis H_job_cost_le_task_cost:
+      cost_of_jobs_from_arrival_sequence_le_task_cost
+        task_cost job_cost job_task arr_seq.
+
+    (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts 
+       [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function 
+       that equals 0 for the empty interval delta = 0. *)
+    Variable max_arrivals: Task -> time -> nat.
+    Hypothesis H_family_of_proper_arrival_curves:
+      family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
+
+    (* Assume we have the model with fixed preemption points. I.e., each task is divided into 
+       a number of nonpreemptive segments by inserting staticaly predefined preemption points. *)
+    Variable job_preemption_points: Job -> seq time.
+    Variable task_preemption_points: Task -> seq time.
+    Hypothesis H_model_with_fixed_preemption_points:
+      fixed_preemption_points_model
+        task_cost job_cost job_task arr_seq
+        job_preemption_points task_preemption_points ts.
+
+    (* Let tsk be any task in ts that is to be analyzed. *)
+    Variable tsk: Task.
+    Hypothesis H_tsk_in_ts: tsk \in ts.
+
+    (* Next, consider any uniprocessor schedule with limited preemptions... *)
+    Variable sched: schedule Job.
+    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
+    Hypothesis H_schedule_with_limited_preemptions:
+      is_schedule_with_limited_preemptions arr_seq job_preemption_points sched.
+
+    (* ... where jobs do not execute before their arrival nor after completion. *)
+    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
+    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+
+    (* Assume we have sequential jobs, i.e, jobs from the same 
+       task execute in the order of their arrival. *)
+    Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
+
+    (* Next, we assume that the schedule is a work-conserving schedule which 
+       respects the JLFP policy under a model with fixed preemption points. *)
+    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
+    Hypothesis H_respects_policy:
+      respects_JLFP_policy_at_preemption_point
+        job_arrival job_cost arr_seq sched
+        (can_be_preempted_for_model_with_limited_preemptions job_preemption_points) higher_eq_priority.
+
+    (* Let's define some local names for clarity. *)
+    Let response_time_bounded_by :=
+      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
+
+    (* We introduce a shortening "rbf" for the task request bound function,
+       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
+    Let rbf := task_request_bound_function task_cost max_arrivals.
+
+    (* Next, we introduce task_rbf as an abbreviation for the task request bound function of task tsk. *)
+    Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
+
+    (* Using the sum of individual request bound functions, we define the request bound 
+       function of all tasks (total request bound function). *)
+    Let total_rbf := total_request_bound_function task_cost max_arrivals ts.
+
+    (* Next, we define an upper bound on interfering workload received from jobs
+       with higher-than-or-equal priority. *)
+    Let W A Δ :=
+      \sum_(tsk_o <- ts | tsk_o != tsk)
+       rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+
+    (* We also have a set of functions that map job or task 
+       to its max or last nonpreemptive segment. *)
+    Let job_max_nps := job_max_nps job_preemption_points.
+    Let job_last_nps := job_last_nps job_preemption_points.
+    Let task_max_nps := task_max_nps task_preemption_points.
+    Let task_last_nps := task_last_nps task_preemption_points.   
+    
+    (* We also define a bound for the priority inversion caused by jobs with lower priority. *)
+    Definition blocking_bound :=
+      \max_(tsk_other <- ts | (tsk_other != tsk) && (D tsk_other > D tsk))
+       (task_max_nps tsk_other - ε).
+    
+    (* Let L be any positive fixed point of the busy interval recurrence, determined by 
+       the sum of blocking and higher-or-equal-priority workload. *)
+    Variable L: time.
+    Hypothesis H_L_positive: L > 0.
+    Hypothesis H_fixed_point: L = blocking_bound + total_rbf L.
+
+    (* To reduce the time complexity of the analysis, recall the notion of search space. *)
+    Let is_in_search_space A :=
+      (A < L)
+        && ((task_rbf A != task_rbf (A + ε))
+            || has (fun tsko =>
+                     (tsk != tsko)
+                       && (rbf tsko (A + D tsk - D tsko)
+                               != rbf tsko ((A + ε) + D tsk - D tsko))) ts).
+
+    (* Next, consider any value R, and assume that for any given arrival A from search space
+       there is a solution of the response-time bound recurrence which is bounded by R. *)
+    Variable R: nat.
+    Hypothesis H_R_is_maximum:
+      forall A,
+        is_in_search_space A -> 
+        exists F,
+          A + F = blocking_bound
+                  + (task_rbf (A + ε) - (task_last_nps tsk - ε)) 
+                  + W A (A + F) /\
+          F + (task_last_nps tsk - ε) <= R.
+
+    (* Now, we can reuse the results for the abstract model of bounded nonpreemptive segments 
+       to establish a response time bound for the concrete model of fixed preemption points.  *)
+    Theorem uniprocessor_response_time_bound_edf_with_fixed_preemption_points:
+      response_time_bounded_by tsk R.  
+    Proof. 
+      move: (H_model_with_fixed_preemption_points) => [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
+      move: (MLP) => [EMPTj [LSMj [BEGj [ENDj HH]]]].
+      move: (posnP (task_cost tsk)) => [ZERO|POSt].
+      { intros j ARR TSK.
+        move: (H_job_cost_le_task_cost _ ARR) => POSt.
+        move: POSt; rewrite /job_cost_le_task_cost TSK ZERO leqn0; move => /eqP Z.
+        rewrite /is_response_time_bound_of_job /completed_by eqn_leq; apply/andP; split.
+        - by eauto 2.
+        - by rewrite Z.
+      } 
+      have Fact2: 1 < size (task_preemption_points tsk).
+      { have Fact2: 0 < size (task_preemption_points tsk).
+        { apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
+          move: (END _ H_tsk_in_ts) => EQ.
+          move: EQ; rewrite /NondecreasingSequence.last -nth_last nth_default; last by rewrite CONTR.
+            by intros; rewrite -EQ in POSt.
+        } 
+        have EQ: 2 = size [::0; task_cost tsk]; first by done. 
+        rewrite EQ; clear EQ.
+        apply subseq_leq_size.
+        rewrite !cons_uniq.
+        { apply/andP; split.
+          rewrite in_cons negb_or; apply/andP; split; last by done.
+          rewrite neq_ltn; apply/orP; left; eauto 2.
+          apply/andP; split; by done. } 
+        intros t EQ; move: EQ; rewrite !in_cons.
+        move => /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
+        { rewrite EQ; clear EQ.
+          move: (BEG _ H_tsk_in_ts) => EQ.
+          rewrite -EQ; clear EQ.
+          rewrite /NondecreasingSequence.first -nth0. 
+          apply/(nthP 0).
+          exists 0; by done.
+        }
+        { rewrite EQ; clear EQ.
+          move: (END _ H_tsk_in_ts) => EQ.
+          rewrite -EQ; clear EQ.
+          rewrite /NondecreasingSequence.last -nth_last.
+          apply/(nthP 0).
+          exists ((size (task_preemption_points tsk)).-1); last by done. 
+            by rewrite -(leq_add2r 1) !addn1 prednK //.
+        }
+      }
+      eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments
+        with (task_lock_in_service := fun tsk => (task_cost tsk - (task_last_nps tsk - ε))) 
+             (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
+             (L0 := L) (job_max_nps0 := job_max_nps)
+             (job_cost0 := job_cost )
+      ; eauto 2.
+      { by apply model_with_fixed_preemption_points_is_correct. }
+      { eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2.
+        intros j ARR. 
+        unfold ModelWithLimitedPreemptions.job_max_nps, task_max_nps, lengths_of_segments.
+        apply NondecreasingSequence.max_of_dominating_seq.
+        intros. apply HYP2.
+          by done.
+      }
+      { split; last split. 
+        { intros j ARR POS.
+          rewrite subn_gt0.
+          rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
+          apply LSMj; try done. 
+          rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
+                  ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
+          apply leq_trans with (job_max_nps j);
+            first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq. 
+          rewrite -ENDj; last by done.
+            by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2. 
+        }  
+        { by intros j ARR; rewrite leq_subLR leq_addl. }
+        { intros ? ? ? ARR LE LS NCOMPL.
+          rewrite subnBA in LS; last first.          
+          apply LSMj; try done.
+          { rewrite lt0n; apply/negP; intros Z; move: Z => /eqP Z.
+            move: NCOMPL; rewrite /completed_by neq_ltn; move => /orP [LT|GT].
+            { by rewrite Z ltn0 in LT. }
+            { move: GT; rewrite ltnNge; move => /negP GT; apply: GT.
+                by eapply H_completed_jobs_dont_execute.
+            }
+          }
+          have EQ: exists Δ, t' = t + Δ.
+          { exists (t' - t); rewrite subnKC; by done. }
+          move: EQ => [Δ EQ]; subst t'; clear LE.
+          rewrite -subh1 in LS.
+          rewrite addn1 in LS.
+          apply H_schedule_with_limited_preemptions; first by done.
+          rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
+          intros CONTR.
+          move: NCOMPL; rewrite /completed_by neq_ltn; move => /orP [SERV|SERV]; last first.
+          { exfalso.
+            move: (H_completed_jobs_dont_execute j (t + Δ)); rewrite leqNgt; move => /negP T.
+              by apply: T.
+          }
+          { have NEQ: job_cost j - job_last_nps j < service sched j (t + Δ).
+            { apply leq_trans with (service sched j t); first by done.
+              rewrite /service /service_during [in X in _ <= X](@big_cat_nat _ _ _ t) //=.
+              rewrite leq_addr //. 
+              rewrite leq_addr //.
+            }
+            clear LS.
+            rewrite -ENDj in NEQ, SERV; last by done.
+            rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ; last by eauto 2.
+            rewrite /NondecreasingSequence.last -nth_last in SERV. 
+            have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
+            specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
+            rewrite CONTR in EQ.
+            feed_n 2 EQ; first by eauto 2.
+            {
+              apply/andP; split; first by done.
+              rewrite prednK; first by done.
+              rewrite -(leq_add2r 1) !addn1 prednK.
+              eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
+              eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2. 
+            }
+              by done.
+          }
+          rewrite -ENDj; last by done.
+          apply leq_trans with (job_max_nps j).
+          - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
+          - by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+        }
+      }
+      {
+        split.
+        - by rewrite /task_lock_in_service_le_task_cost leq_subLR leq_addl.
+        - intros j ARR TSK.
+          move: (posnP (job_cost j)) => [ZERO | POS].
+          { by rewrite ZERO. } 
+          unfold task_last_nps.
+          rewrite !subnBA; first last.
+          apply LSMj; try done.
+          rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
+          apply HYP3.
+            by done.
+            rewrite -(ltn_add2r 1) !addn1 prednK //.
+          move: (Fact2) => Fact3.
+          rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2. 
+          rewrite -subh1 -?[in X in _ <= X]subh1; first last. 
+          { apply leq_trans with (job_max_nps j).
+            - by apply NondecreasingSequence.last_of_seq_le_max_of_seq. 
+            - by rewrite -ENDj //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+          } 
+          { apply leq_trans with (task_max_nps tsk). 
+            - by apply NondecreasingSequence.last_of_seq_le_max_of_seq. 
+            - by rewrite -END //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+          }
+          rewrite -ENDj; last eauto 2.
+          rewrite -END; last eauto 2.
+          rewrite !NondecreasingSequence.last_seq_minus_last_distance_seq.
+          have EQ: size (job_preemption_points j) = size (task_preemption_points tsk).
+          { rewrite -TSK.
+              by apply HYP1.
+          }
+          rewrite EQ; clear EQ. 
+          rewrite leq_add2r.
+          apply NondecreasingSequence.domination_of_distances_implies_domination_of_seq; try done; eauto 2. 
+          rewrite BEG // BEGj //.
+          eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
+          rewrite -TSK; apply HYP1; try done.
+                    intros.              rewrite -TSK; eauto 2.
+                    eauto 2.
+                    eauto 2.
+      }
+      { rewrite subKn; first by done.
+        rewrite /task_last_nps  -(leq_add2r 1) subn1 !addn1 prednK; last first.
+        { rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
+          apply HYP3; try by done. 
+          rewrite -(ltn_add2r 1) !addn1 prednK //.
+          move: (Fact2) => Fact3.
+            by rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2.
+        }        
+        { apply leq_trans with (task_max_nps tsk).
+          - by apply NondecreasingSequence.last_of_seq_le_max_of_seq. 
+          - rewrite -END; last by done.
+            apply ltnW; rewrite ltnS; try done.
+              by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2. 
+        }
+      }
+    Qed.
+     
+  End Analysis. 
+   
+End RTAforFixedPreemptionPointsModelwithArrivalCurves.
\ No newline at end of file

model/schedule/uni/limited/edf/nonpr_reg/floating/response_time_bound.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job
+               rt.model.arrival.basic.task_arrival
+               rt.model.priority.
+Require Import rt.model.schedule.uni.service
+               rt.model.schedule.uni.workload
+               rt.model.schedule.uni.schedule
+               rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.limited.schedule
+               rt.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound
+               rt.model.schedule.uni.limited.rbf.
+Require Import rt.model.arrival.curves.bounds. 
+Require Import rt.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.model.schedule.uni.limited.platform.limited.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+ 
+(** * RTA for EDF-schedulers with floating nonpreemptive regions *)
+(** In this module we prove a general RTA theorem for EDF-schedulers with floating nonpreemptive regions *)
+Module RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
+
+  Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+         ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
+         RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
+
+  Section Analysis.
+
+    Context {Task: eqType}.
+    Variable task_cost: Task -> time.
+    Variable task_deadline: Task -> time.
+
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+
+    (* For clarity, let's denote the relative deadline of a task as D. *)
+    Let D tsk := task_deadline tsk.
+    
+    (* The deadline of a job is equal to the deadline of the corresponding task. *)
+    Let job_deadline j := D (job_task j).
+
+    (* Consider the EDF policy that indicates a higher-or-equal priority relation. *)
+    Let higher_eq_priority: JLFP_policy Job := EDF job_arrival job_deadline.
+
+    (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+    (* Consider an arbitrary task set ts. *)
+    Variable ts: list Task.
+
+    (* Assume that all jobs come from the task set... *)
+    Hypothesis H_all_jobs_from_taskset:
+      forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+    (* ...and the cost of a job cannot be larger than the task cost. *)
+    Hypothesis H_job_cost_le_task_cost:
+      cost_of_jobs_from_arrival_sequence_le_task_cost
+        task_cost job_cost job_task arr_seq.
+
+    (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts 
+       [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function 
+       that equals 0 for the empty interval delta = 0. *)
+    Variable max_arrivals: Task -> time -> nat.
+    Hypothesis H_family_of_proper_arrival_curves:
+      family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
+
+    (* Assume we have model with floating nonpreemptive regions. I.e., for each
+       task only the length of the maximal nonpreemptive segment is known. *)
+    Variable job_preemption_points: Job -> seq time.
+    Variable task_max_nps: Task -> time.
+    Hypothesis H_task_model_with_floating_nonpreemptive_regions:
+      model_with_floating_nonpreemptive_regions
+        job_cost job_task arr_seq job_preemption_points task_max_nps.
+
+    (* Let tsk be any task in ts that is to be analyzed. *)
+    Variable tsk: Task.
+    Hypothesis H_tsk_in_ts: tsk \in ts.
+
+    (* Next, consider any uniprocessor schedule with limited preemptions... *)
+    Variable sched: schedule Job.
+    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
+    Hypothesis H_schedule_with_limited_preemptions:
+      is_schedule_with_limited_preemptions arr_seq job_preemption_points sched.
+
+    (* ... where jobs do not execute before their arrival nor after completion. *)
+    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
+    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+
+    (* Assume we have sequential jobs, i.e, jobs from the same 
+       task execute in the order of their arrival. *)
+    Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
+
+    (* Next, we assume that the schedule is a work-conserving schedule which 
+       respects the JLFP policy under a model with floating nonpreemptive regions. *)
+    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
+    Hypothesis H_respects_policy:
+      respects_JLFP_policy_at_preemption_point
+        job_arrival job_cost arr_seq sched
+        (can_be_preempted_for_model_with_limited_preemptions job_preemption_points) higher_eq_priority.
+
+    (* Let's define some local names for clarity. *)
+    Let response_time_bounded_by :=
+      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
+
+    (* We introduce a shortening "rbf" for the task request bound function
+       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
+    Let rbf := task_request_bound_function task_cost max_arrivals.
+
+    (* Next, we introduce task_rbf as an abbreviation for the task request bound function of task tsk. *)
+    Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
+
+    (* Using the sum of individual request bound functions, we define the request bound 
+       function of all tasks (total request bound function). *)
+    Let total_rbf := total_request_bound_function task_cost max_arrivals ts.
+
+    (* Next, we define an upper bound on interfering workload received from jobs
+       with higher-than-or-equal priority. *)
+    Let W A Δ :=
+      \sum_(tsk_o <- ts | tsk_o != tsk)
+       rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+
+    (* We also have two functions that map job to its max or last nonpreemptive segment. *)
+    Let job_max_nps := job_max_nps job_preemption_points.
+    Let job_last_nps := job_last_nps job_preemption_points.
+
+    (* We also define a bound for the priority inversion caused by jobs with lower priority. *)
+    Definition blocking_bound :=
+      \max_(tsk_other <- ts | (tsk_other != tsk) && (D tsk_other > D tsk))
+       (task_max_nps tsk_other - ε).
+
+    (* Let L be any positive fixed point of the busy interval recurrence, determined by 
+       the sum of blocking and higher-or-equal-priority workload. *)
+    Variable L: time.
+    Hypothesis H_L_positive: L > 0.
+    Hypothesis H_fixed_point: L = blocking_bound + total_rbf L.
+
+    (* To reduce the time complexity of the analysis, recall the notion of search space. *)
+    Let is_in_search_space A :=
+      (A < L)
+        && ((task_rbf A != task_rbf (A + ε))
+            || has (fun tsko =>
+                     (tsk != tsko) && (rbf tsko (A + D tsk - D tsko)
+                                    != rbf tsko ((A + ε) + D tsk - D tsko))) ts).
+
+    (* Next, consider any value R, and assume that for any given arrival A from search space
+       there is a solution of the response-time bound recurrence which is bounded by R. *)
+    Variable R: nat.
+    Hypothesis H_R_is_maximum:
+      forall A,
+        is_in_search_space A -> 
+        exists F,
+          A + F = blocking_bound + task_rbf (A + ε) + W A (A + F) /\
+          F <= R.
+
+    (* Now, we can reuse the results for the abstract model of bounded nonpreemptive segments 
+       to establish a response time bound for the concrete model with floating nonpreemptive regions.  *)
+    Theorem uniprocessor_response_time_bound_edf_with_floating_nonpreemptive_regions:
+      response_time_bounded_by tsk R.  
+    Proof.
+      move: (H_task_model_with_floating_nonpreemptive_regions) => [LIMJ JMLETM].
+      move: (LIMJ) => [ZERO [LSMj [BEG [END HH]]]].
+      eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments
+        with (task_lock_in_service := fun tsk => task_cost tsk) 
+             (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
+             (L0 := L) (job_max_nps0 := job_max_nps)
+             (job_cost0 := job_cost )
+      ; eauto 2.
+      { by apply model_with_fixed_preemption_points_is_correct. }
+      { by eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2. }
+      { split; last split.
+        { intros j ARR POS.
+          rewrite subn_gt0.
+          rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
+          apply LSMj; try done.
+          rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
+                  ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
+          apply leq_trans with (job_max_nps j); first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq.
+          rewrite -END; last by done.
+            by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+        }  
+        { by intros j ARR; rewrite leq_subLR leq_addl. }
+        { intros ? ? ? ARR LE LS NCOMPL.  
+          rewrite subnBA in LS; last first.
+          apply LSMj; try done.
+          { rewrite lt0n; apply/negP; intros Z; move: Z => /eqP Z.
+            move: NCOMPL. rewrite /completed_by neq_ltn. move => /orP [LT|GT].
+            { by rewrite Z ltn0 in LT. }
+            { move: GT; rewrite ltnNge; move => /negP GT; apply: GT.
+                by eapply H_completed_jobs_dont_execute.
+            }
+          }
+          have EQ: exists Δ, t' = t + Δ.
+          { exists (t' - t); rewrite subnKC; by done. }
+          move: EQ => [Δ EQ]; subst t'; clear LE.
+          rewrite -subh1 in LS.
+          rewrite addn1 in LS.
+          apply H_schedule_with_limited_preemptions; first by done.
+          rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
+          intros CONTR.
+          move: NCOMPL; rewrite /completed_by neq_ltn; move => /orP [SERV|SERV]; last first.
+          { exfalso.
+            move: (H_completed_jobs_dont_execute j (t + Δ)); rewrite leqNgt; move => /negP T.
+              by apply: T.
+          }
+          { have NEQ: job_cost j - (job_last_nps j) < service sched j (t + Δ).
+            { apply leq_trans with (service sched j t); first by done.
+              rewrite /service /service_during [in X in _ <= X](@big_cat_nat _ _ _ t) //=.
+              rewrite leq_addr //.
+              rewrite leq_addr //.
+            }
+            clear LS.
+            rewrite -END in NEQ, SERV; last by done.
+            rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ.
+            rewrite /NondecreasingSequence.last -nth_last in SERV. 
+            have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
+            specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
+            rewrite CONTR in EQ.
+            feed_n 2 EQ; first by eauto 2.
+            {
+              apply/andP; split; first by done.
+              rewrite prednK; first by done.
+              rewrite -(leq_add2r 1) !addn1 prednK.
+              eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2. 
+              eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2. 
+            }
+              by done.
+            eauto 2.
+          }
+          rewrite -END; last by done.
+          apply leq_trans with (job_max_nps j).
+          - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
+          - by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+        }
+      }
+      {
+        split.
+        - by rewrite /task_lock_in_service_le_task_cost. 
+        - intros j ARR TSK.
+          apply leq_trans with (job_cost j); first by rewrite leq_subr.
+            by rewrite -TSK; eauto 2.
+      }
+      {
+        rewrite subnn.
+        intros.
+        apply H_R_is_maximum in H.
+        move: H => [F [EQ LE]].
+        exists F.
+          by rewrite subn0 addn0; split.
+      }
+    Qed.
+     
+  End Analysis.
+    
+End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves. 
\ No newline at end of file

model/schedule/uni/limited/edf/nonpr_reg/nonpreemptive/response_time_bound.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
+Require Import rt.model.schedule.uni.service
+               rt.model.schedule.uni.workload
+               rt.model.schedule.uni.schedule 
+               rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.nonpreemptive.schedule.
+Require Import rt.model.schedule.uni.limited.schedule
+               rt.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound.
+Require Import rt.model.arrival.curves.bounds.
+Require Import rt.analysis.uni.arrival_curves.workload_bound.
+
+Require Import rt.model.schedule.uni.limited.platform.nonpreemptive.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * RTA for fully nonpreemptive EDF model *)
+(** In this module we prove the RTA theorem for the fully nonpreemptive EDF model. *)
+Module RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
+
+  Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule
+         NonpreemptiveSchedule Workload Service FullyNonPreemptivePlatform
+         ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform
+         RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
+  
+  Section Analysis.
+
+    Context {Task: eqType}.
+    Variable task_cost: Task -> time.
+    Variable task_deadline: Task -> time.
+
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+
+    (* For clarity, let's denote the relative deadline of a task as D. *)
+    Let D tsk := task_deadline tsk.
+
+    (* The deadline of a job is equal to the deadline of the corresponding task. *)
+    Let job_deadline j := D (job_task j).
+
+    (* Consider the EDF policy that indicates a higher-or-equal priority relation. *)
+    Let higher_eq_priority: JLFP_policy Job := EDF job_arrival job_deadline.
+
+    (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+    (* Consider an arbitrary task set ts. *)
+    Variable ts: list Task.
+
+    (* Assume that all jobs come from the task set... *)
+    Hypothesis H_all_jobs_from_taskset:
+      forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+    (* ...and the cost of a job cannot be larger than the task cost. *)
+    Hypothesis H_job_cost_le_task_cost:
+      cost_of_jobs_from_arrival_sequence_le_task_cost
+        task_cost job_cost job_task arr_seq.
+
+    (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts 
+       [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function 
+       that equals 0 for the empty interval delta = 0. *)
+    Variable max_arrivals: Task -> time -> nat.
+    Hypothesis H_family_of_proper_arrival_curves:
+      family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
+
+    (* Let tsk be any task in ts that is to be analyzed. *)
+    Variable tsk: Task.
+    Hypothesis H_tsk_in_ts: tsk \in ts.
+
+    (* Next, consider any uniprocessor nonpreemptive schedule...*)
+    Variable sched: schedule Job.
+    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
+    Hypothesis H_nonpreemptive_sched: is_nonpreemptive_schedule job_cost sched.
+
+    (* ... where jobs do not execute before their arrival nor after completion. *)
+    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
+    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+
+    (* Assume we have sequential jobs, i.e, jobs from the same 
+       task execute in the order of their arrival. *)
+    Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
+
+    (* Next, we assume that the schedule is a work-conserving schedule which 
+       respects the JLFP policy under a model with fixed preemption points. *)
+    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
+    Hypothesis H_respects_policy:
+      respects_JLFP_policy_at_preemption_point
+        job_arrival job_cost arr_seq sched
+        (can_be_preempted_for_fully_nonpreemptive_model job_cost) higher_eq_priority.
+
+    (* Let's define some local names for clarity. *)
+    Let response_time_bounded_by :=
+      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
+
+    (* We introduce a shortening "rbf" for the task request bound function,
+       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
+    Let rbf := task_request_bound_function task_cost max_arrivals.
+
+    (* Next, we introduce task_rbf as an abbreviation for the task request bound function of task tsk. *)
+    Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
+
+    (* Using the sum of individual request bound functions, we define the request bound 
+       function of all tasks (total request bound function). *)
+    Let total_rbf := total_request_bound_function task_cost max_arrivals ts.
+
+    (* Next, we define an upper bound on interfering workload received from jobs
+       with higher-than-or-equal priority. *)
+    Let W A Δ :=
+      \sum_(tsk_o <- ts | tsk_o != tsk)
+       rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+
+    (* We also define a bound for the priority inversion caused by jobs with lower priority. *)
+    Definition blocking_bound :=
+      \max_(tsk_other <- ts | (tsk_other != tsk) && (D tsk_other > D tsk))
+       (task_cost tsk_other - ε).
+
+    (* Let L be any positive fixed point of the busy interval recurrence, determined by 
+       the sum of blocking and higher-or-equal-priority workload. *)
+    Variable L: time.
+    Hypothesis H_L_positive: L > 0.
+    Hypothesis H_fixed_point: L = blocking_bound + total_rbf L.
+
+    (* To reduce the time complexity of the analysis, recall the notion of search space. *)
+    Let is_in_search_space A :=
+      (A < L)
+        && ((task_rbf A != task_rbf (A + ε))
+            || has (fun tsko =>
+                     (tsk != tsko)
+                       && (rbf tsko (A + D tsk - D tsko)
+                               != rbf tsko ((A + ε) + D tsk - D tsko))) ts).
+
+    (* Next, consider any value R, and assume that for any given arrival A from search space
+       there is a solution of the response-time bound recurrence which is bounded by R. *)
+    Variable R: nat.
+    Hypothesis H_R_is_maximum:
+      forall A,
+        is_in_search_space A -> 
+        exists F,
+          A + F = blocking_bound + (task_rbf (A + ε) - (task_cost tsk - ε)) + W A (A + F) /\
+          F + (task_cost tsk - ε) <= R.
+
+    (* Now, we can reuse the results for the abstract model with fixed preemption points to 
+       establish a response-time bound for the more concrete model of fully nonpreemptive scheduling. *)
+    Theorem uniprocessor_response_time_bound_fully_nonpreemptive_edf:
+      response_time_bounded_by tsk R.
+    Proof.
+      move: (posnP (task_cost tsk)) => [ZERO|POS].
+      { intros j ARR TSK.
+        have ZEROj: job_cost j = 0.
+        { move: (H_job_cost_le_task_cost j ARR) => NEQ.
+          rewrite /job_cost_le_task_cost TSK ZERO in NEQ.
+            by apply/eqP; rewrite -leqn0.
+        }
+        rewrite /is_response_time_bound_of_job /completed_by eqn_leq; apply/andP; split.
+        - by apply H_completed_jobs_dont_execute.
+        - by rewrite ZEROj.
+      }
+      eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with
+        (job_max_nps := fun j => job_cost j)
+        (task_max_nps := fun tsk => task_cost tsk)
+        (job_lock_in_service := fun j => ε)
+        (task_lock_in_service := fun tsk => ε)
+        (L0 := L); eauto 2.
+      - by eapply fully_nonpreemptive_model_is_correct; eauto 2.
+      - eapply fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions; eauto 2.
+      - repeat split; try done.
+      - intros j t t' ARR LE SERV NCOMPL.
+        rewrite /service in SERV; apply incremental_service_during in SERV.
+        move: SERV => [t_first [/andP [_ H1] [H2 H3]]].
+        apply H_nonpreemptive_sched with t_first; try done.
+          by apply leq_trans with t; first apply ltnW.
+      - repeat split; try done.
+    Qed.
+    
+  End Analysis.
+   
+End RTAforFullyNonPreemptiveEDFModelwithArrivalCurves. 
\ No newline at end of file

model/schedule/uni/limited/edf/nonpr_reg/preemptive/response_time_bound.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
+Require Import rt.model.schedule.uni.service
+               rt.model.schedule.uni.workload
+               rt.model.schedule.uni.schedule
+               rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.limited.platform.preemptive
+               rt.model.schedule.uni.limited.schedule
+               rt.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound.
+Require Import rt.model.arrival.curves.bounds.
+Require Import rt.analysis.uni.arrival_curves.workload_bound.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * RTA for fully preemptive EDF model *)
+(** In this module we prove the RTA theorem for fully preemptive EDF model *)
+Module RTAforFullyPreemptiveEDFModelwithArrivalCurves. 
+               
+  Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+         ResponseTime MaxArrivalsWorkloadBound FullyPreemptivePlatform LimitedPreemptionPlatform
+         RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
+
+  Section Analysis.
+
+    Context {Task: eqType}.
+    Variable task_cost: Task -> time.
+    Variable task_deadline: Task -> time.
+
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+    
+    (* For clarity, let's denote the relative deadline of a task as D. *)
+    Let D tsk := task_deadline tsk.
+
+    (* The deadline of a job is equal to the deadline of the corresponding task. *)
+    Let job_deadline j := D (job_task j).
+
+    (* Consider the EDF policy that indicates a higher-or-equal priority relation. *)
+    Let higher_eq_priority: JLFP_policy Job := EDF job_arrival job_deadline.
+
+    (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+    (* Consider an arbitrary task set ts. *)
+    Variable ts: list Task.
+
+    (* Assume that all jobs come from the task set... *)
+    Hypothesis H_all_jobs_from_taskset:
+      forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+    (* ...and the cost of a job cannot be larger than the task cost. *)
+    Hypothesis H_job_cost_le_task_cost:
+      cost_of_jobs_from_arrival_sequence_le_task_cost
+        task_cost job_cost job_task arr_seq.
+
+    (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts 
+       [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function 
+       that equals 0 for the empty interval delta = 0. *)
+    Variable max_arrivals: Task -> time -> nat.
+    Hypothesis H_family_of_proper_arrival_curves:
+      family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
+
+    (* Let tsk be any task in ts that is to be analyzed. *)
+    Variable tsk: Task.
+    Hypothesis H_tsk_in_ts: tsk \in ts.
+
+    (* Next, consider any uniprocessor schedule... *)
+    Variable sched: schedule Job.
+    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
+
+    (* ... where jobs do not execute before their arrival nor after completion. *)
+    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
+    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+
+    (* Assume we have sequential jobs, i.e, jobs from the same 
+       task execute in the order of their arrival. *)
+    Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
+
+    (* Next, we assume that the schedule is a work-conserving schedule which 
+       respects the JLFP policy under a model with fixed preemption points. *)
+    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
+    Hypothesis H_respects_policy:
+      respects_JLFP_policy_at_preemption_point
+        job_arrival job_cost arr_seq sched
+        can_be_preempted_for_fully_preemptive_model higher_eq_priority.
+
+    (* Let's define some local names for clarity. *)
+    Let response_time_bounded_by :=
+      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
+
+    (* We introduce a shortening "rbf" for the task request bound function,
+       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
+    Let rbf := task_request_bound_function task_cost max_arrivals.
+
+    (* Next, we introduce task_rbf as an abbreviation for the task request bound function of task tsk. *)
+    Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
+
+    (* Using the sum of individual request bound functions, we define the request bound 
+       function of all tasks (total request bound function). *)
+    Let total_rbf := total_request_bound_function task_cost max_arrivals ts.
+
+    (* Next, we define an upper bound on interfering workload received from jobs
+       with higher-than-or-equal priority. *)
+    Let W A Δ :=
+      \sum_(tsk_o <- ts | tsk_o != tsk)
+       rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+
+    (* Let L be any positive fixed point of the busy interval recurrence, determined by 
+       the sum of blocking and higher-or-equal-priority workload. *)
+    Variable L: time.
+    Hypothesis H_L_positive: L > 0.
+    Hypothesis H_fixed_point: L = total_rbf L.
+
+    (* To reduce the time complexity of the analysis, recall the notion of search space. *)
+    Let is_in_search_space A :=
+      (A < L)
+        && ((task_rbf A != task_rbf (A + ε))
+            || has (fun tsko =>
+                     (tsk != tsko)
+                       && (rbf tsko (A + D tsk - D tsko)
+                               != rbf tsko ((A + ε) + D tsk - D tsko))) ts).
+
+    (* Next, consider any value R, and assume that for any given arrival A from search space
+       there is a solution of the response-time bound recurrence which is bounded by R. *)
+    Variable R: nat.
+    Hypothesis H_R_is_maximum:
+      forall A,
+        is_in_search_space A -> 
+        exists F,
+          A + F = task_rbf (A + ε) + W A (A + F) /\
+          F <= R.
+
+    (* Now, we can reuse the results for the abstract model with fixed preemption 
+       points to establish a response-time bound for the more concrete model 
+       of fully-preemptive scheduling. *)
+    Theorem uniprocessor_response_time_bound_fully_preemptive_edf:
+      response_time_bounded_by tsk R.
+    Proof.
+      have BLOCK: RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.blocking_bound
+                    (fun _ => ε) D ts tsk = 0.
+      { by rewrite /RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.blocking_bound subnn big1_eq. } 
+      eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with
+          (task_max_nps := fun _ => ε)
+          (can_be_preempted := fun j prog => true)
+          (task_lock_in_service := fun tsk => task_cost tsk)
+          (job_lock_in_service := fun j => job_cost j)
+          (job_max_nps := fun j => ε); eauto 2; try done.
+      - by eapply fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions.
+      - repeat split; try done.
+        intros ? ? ? ARR; move => LE COMPL /negP NCOMPL.
+        exfalso; apply: NCOMPL.
+        apply completion_monotonic with t; try done.
+        rewrite /completed_by eqn_leq; apply/andP; split; try done.
+      - repeat split; try done. 
+        rewrite /task_lock_in_service_le_task_cost. by done.
+        unfold task_lock_in_service_bounds_job_lock_in_service.
+          by intros ? ARR TSK; rewrite -TSK; apply H_job_cost_le_task_cost. 
+      - by rewrite BLOCK add0n.
+      - move => A /andP [LT NEQ].
+        specialize (H_R_is_maximum A); feed H_R_is_maximum.
+        { by apply/andP; split. }
+        move: H_R_is_maximum => [F [FIX BOUND]].
+        exists F; split.
+        + by rewrite BLOCK add0n subnn subn0. 
+        + by rewrite subnn addn0. 
+    Qed.
+    
+  End Analysis.
+  
+End RTAforFullyPreemptiveEDFModelwithArrivalCurves. 
\ No newline at end of file

model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job
+               rt.model.arrival.basic.task_arrival
+               rt.model.priority.
+Require Import rt.model.schedule.uni.service
+               rt.model.schedule.uni.workload
+               rt.model.schedule.uni.schedule
+               rt.model.schedule.uni.response_time. 
+Require Import rt.model.schedule.uni.limited.platform.definitions
+               rt.model.schedule.uni.limited.platform.priority_inversion_is_bounded
+               rt.model.schedule.uni.limited.schedule
+               rt.model.schedule.uni.limited.busy_interval
+               rt.model.schedule.uni.limited.edf.response_time_bound
+               rt.model.schedule.uni.limited.rbf.
+Require Import rt.model.arrival.curves.bounds.
+Require Import rt.analysis.uni.arrival_curves.workload_bound.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * RTA for EDF-schedulers with bounded nonpreemprive segments *)
+(** In this module we prove a general RTA theorem for EDF-schedulers. *)
+Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
+
+  Import Epsilon Job ArrivalCurves TaskArrival Priority  UniprocessorSchedule Workload Service
+         ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform RBF 
+         AbstractRTAforEDFwithArrivalCurves BusyIntervalJLFP PriorityInversionIsBounded. 
+
+  Section Analysis.
+
+    Context {Task: eqType}.
+    Variable task_max_nps task_cost: Task -> time.
+    Variable task_deadline: Task -> time.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_max_nps job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+    
+    (* For clarity, let's denote the relative deadline of a task as D. *)
+    Let D tsk := task_deadline tsk.
+
+    (* The deadline of a job is equal to the deadline of the corresponding task. *)
+    Let job_deadline j := D (job_task j).
+
+    (* Consider any arrival sequence with consistent, non-duplicate arrivals... *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
+    
+    (* Next, consider any uniprocessor schedule of this arrival sequence...*)
+    Variable sched: schedule Job.
+    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
+
+    (* ... where jobs do not execute before their arrival nor after completion. *)
+    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
+    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+
+    (* Assume we have sequential jobs, i.e, jobs from the same 
+       task execute in the order of their arrival. *)
+    Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
+
+    (* Consider the EDF policy that indicates a higher-or-equal priority relation. *)
+    Let higher_eq_priority: JLFP_policy Job := EDF job_arrival job_deadline.
+    
+    (* We consider an arbitrary function can_be_preempted which defines 
+       a preemption model with bounded nonpreemptive segments. *)
+    Variable can_be_preempted: Job -> time -> bool.
+    Let preemption_time := preemption_time sched can_be_preempted.
+    Hypothesis H_correct_preemption_model:
+      correct_preemption_model arr_seq sched can_be_preempted.
+    Hypothesis H_model_with_bounded_nonpreemptive_segments:
+      model_with_bounded_nonpreemptive_segments
+        job_cost job_task arr_seq can_be_preempted job_max_nps task_max_nps.
+    
+    (* Next, we assume that the schedule is a work-conserving schedule... *)
+    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
+
+    (* ... and the schedule respects the policy defined by the 
+       can_be_preempted function (i.e., bounded nonpreemptive segments). *)
+    Hypothesis H_respects_policy:
+      respects_JLFP_policy_at_preemption_point
+        job_arrival job_cost arr_seq sched can_be_preempted higher_eq_priority.
+    
+    (* Consider an arbitrary task set ts. *)
+    Variable ts: list Task.
+    
+    (* Assume that all jobs come from the task set... *)
+    Hypothesis H_all_jobs_from_taskset:
+      forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+    (* ...and the cost of a job cannot be larger than the task cost. *)
+    Hypothesis H_job_cost_le_task_cost:
+      cost_of_jobs_from_arrival_sequence_le_task_cost
+        task_cost job_cost job_task arr_seq.
+
+    (* Let tsk be any task in ts that is to be analyzed. *)
+    Variable tsk: Task.
+    Hypothesis H_tsk_in_ts: tsk \in ts.
+    
+   (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts 
+      [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function 
+      that equals 0 for the empty interval delta = 0. *)
+    Variable max_arrivals: Task -> time -> nat.
+    Hypothesis H_family_of_proper_arrival_curves:
+      family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
+    
+    (* Consider a proper job lock-in service and task lock-in functions, i.e... *)
+    Variable job_lock_in_service: Job -> time.
+    Variable task_lock_in_service: Task -> time.
+
+    (* ...we assume that for all jobs in the arrival sequence the lock-in service is 
+       (1) positive, (2) no bigger than costs of the corresponding jobs, and (3) a job
+       becomes nonpreemptive after it reaches its lock-in service... *)
+    Hypothesis H_proper_job_lock_in_service:
+      proper_job_lock_in_service job_cost arr_seq sched job_lock_in_service.
+
+    (* ...and that [task_lock_in_service tsk] is (1) no bigger than tsk's cost, (2) for any
+       job of task tsk job_lock_in_service is bounded by task_lock_in_service. *)
+    Hypothesis H_proper_task_lock_in_service:
+      proper_task_lock_in_service
+        task_cost job_task arr_seq job_lock_in_service task_lock_in_service tsk.
+
+    (* We introduce a shortening "rbf" for the task request bound function,
+       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
+    Let rbf := task_request_bound_function task_cost max_arrivals.
+
+    (* Next, we introduce task_rbf as an abbreviation for the task
+       request bound function of task tsk. *)
+    Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
+
+    (* Using the sum of individual request bound functions, we define the request bound 
+       function of all tasks (total request bound function). *)
+    Let total_rbf := total_request_bound_function task_cost max_arrivals ts.
+
+    (* Next, we define an upper bound on interfering workload received from jobs
+       with higher-than-or-equal priority. *)
+    Let W A Δ :=
+      \sum_(tsk_o <- ts | tsk_o != tsk)
+       rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+
+    (* Let's define some local names for clarity. *)
+    Let job_pending_at := pending job_arrival job_cost sched.
+    Let job_scheduled_at := scheduled_at sched.
+    Let job_completed_by := completed_by job_cost sched.
+    Let job_backlogged_at := backlogged job_arrival job_cost sched.
+    Let arrivals_between := jobs_arrived_between arr_seq.
+    Let response_time_bounded_by :=
+      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
+    Let max_length_of_priority_inversion :=
+      max_length_of_priority_inversion job_max_nps arr_seq higher_eq_priority.
+    
+    (* We also define a bound for the priority inversion caused by jobs with lower priority. *)
+    Definition blocking_bound :=
+      \max_(tsk_other <- ts | (tsk_other != tsk) && (D tsk < D tsk_other))
+       (task_max_nps tsk_other - ε).
+    
+    (** ** Priority inversion is bounded *)
+    (** In this section, we prove that a priority inversion for task tsk is bounded by 
+        the maximum length of nonpreemtive segments among the tasks with lower priority. *)
+    Section PriorityInversionIsBounded.
+
+      (* First, we prove that the maximum length of a priority inversion of job j is 
+         bounded by the maximum length of a nonpreemptive section of a task with 
+         lower-priority task (i.e., the blocking term). *)
+      Lemma priority_inversion_is_bounded_by_blocking:
+        forall j t,
+          arrives_in arr_seq j ->
+          job_task j = tsk ->
+          t <= job_arrival j ->
+          max_length_of_priority_inversion j t <= blocking_bound.
+      Proof.
+        intros j t ARR TSK LE.  
+        unfold max_length_of_priority_inversion, blocking_bound. 
+        apply leq_trans with
+            (\max_(j_lp <- jobs_arrived_between arr_seq 0 t |
+                   ~~ higher_eq_priority j_lp j)
+              (task_max_nps (job_task j_lp) - ε)
+            ).
+        { apply leq_big_max.
+          intros j' JINB NOTHEP. 
+          specialize (H_job_cost_le_task_cost j').
+          feed H_job_cost_le_task_cost.
+          { apply mem_bigcat_nat_exists in JINB.
+              by move: JINB => [ta' [JIN' _]]; exists ta'.
+          }
+          rewrite leq_sub2r //.
+          apply in_arrivals_implies_arrived in JINB.
+          move: (H_model_with_bounded_nonpreemptive_segments j' JINB) => [_ [_ [T _]]].
+            by apply T.
+        }
+        { apply /bigmax_leq_seqP. 
+          intros j' JINB NOTHEP.
+          apply leq_bigmax_cond_seq with
+              (i0 := (job_task j')) (F := fun tsk => task_max_nps tsk - 1). 
+          { apply H_all_jobs_from_taskset.
+            apply mem_bigcat_nat_exists in JINB.
+              by inversion JINB as [ta' [JIN' _]]; exists ta'. }
+          { have NINTSK: job_task j' != tsk.
+            { apply/eqP; intros TSKj'.
+              rewrite /higher_eq_priority /EDF -ltnNge in NOTHEP.
+              rewrite /job_deadline TSKj' TSK ltn_add2r in NOTHEP.
+              move: NOTHEP; rewrite ltnNge; move => /negP T; apply: T.
+              apply leq_trans with t; last by done.
+              eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.
+              move: JINB; move => /andP [_ T].
+                by apply ltnW.
+            }
+            apply/andP; split; first by done.
+            rewrite /higher_eq_priority /EDF /job_deadline -ltnNge in NOTHEP.
+            rewrite -TSK.
+            have ARRLE: job_arrival j' < job_arrival j.
+            { apply leq_trans with t; last by done.
+              eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.
+                by move: JINB; move => /andP [_ T].
+            }
+            have F: forall a b c d, a + b < c + d -> a > c -> b < d.
+            { clear.
+              intros.
+              rewrite -addn1 -addnA -leq_subLR -subh1 in H; last by apply ltnW.
+              rewrite addn1 addnS in H.
+              rewrite -subn_gt0 in H0.
+              apply ltn_trans with (a - c + b); last by done.
+              apply ltn_subLR.
+              have EQ: b - b = 0. apply/eqP. rewrite subn_eq0. by done.
+                by rewrite EQ.
+            }
+            eapply F; eauto 2.
+          }
+        }
+      Qed.
+        
+      (* Using the lemmas above, we prove that the priority inversion of the task is bounded by 
+         the maximum length of a nonpreemptive section of lower-priority tasks. *)
+      Lemma priority_inversion_is_bounded:
+        priority_inversion_is_bounded_by
+          job_arrival job_cost job_task arr_seq sched higher_eq_priority tsk blocking_bound.
+      Proof.
+        intros j ARR TSK POS t1 t2 PREF.
+        move: (PREF) => [_ [_ [_ /andP [T _]]]].
+        case NEQ: (t2 - t1 <= blocking_bound). 
+        { apply leq_trans with (t2 - t1); last by done.
+          rewrite /cumulative_priority_inversion /is_priority_inversion. 
+          rewrite -[X in _ <= X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat. 
+          rewrite leq_sum //.
+          intros t _; case: (sched t); last by done.
+            by intros s; case: (higher_eq_priority).
+        }
+        move: NEQ => /negP /negP; rewrite -ltnNge; move => NEQ. 
+        have PPE := preemption_time_exists
+                      task_max_nps job_arrival job_max_nps job_cost job_task arr_seq
+                      _ sched _ _ _ higher_eq_priority _ _ can_be_preempted
+                      _ _ _ _ j _ _ t1 t2.
+        feed_n 13 PPE; try done.
+        { by apply EDF_is_reflexive. }
+        { by apply EDF_is_transitive. }
+        move: PPE => [ppt [PPT /andP [GE LE]]].
+        apply leq_trans with (cumulative_priority_inversion sched higher_eq_priority j t1 ppt);
+          last apply leq_trans with (ppt - t1).
+        { rewrite /cumulative_priority_inversion /is_priority_inversion. 
+          rewrite (@big_cat_nat _ _ _ ppt) //=.
+          rewrite -[X in _ <= X]addn0 leq_add2l.
+          rewrite leqn0.
+          rewrite big_nat_cond big1 //; move => t /andP [/andP [GEt LTt] _ ].
+          case SCHED: (sched t) => [s | ]; last by done.
+          have SCHEDHP := not_quiet_implies_exists_scheduled_hp_job
+                            task_max_nps job_arrival job_max_nps job_cost job_task arr_seq
+                            _ sched _ _ _ higher_eq_priority _ _ can_be_preempted
+                            _ _ _ _ j _  _ t1 t2 _ (ppt - t1) _ t.
+          feed_n 15 SCHEDHP; try done.
+          { by apply EDF_is_reflexive. }
+          { by apply EDF_is_transitive. }
+          { exists ppt; split.  by done.  by rewrite subnKC //; apply/andP; split. } 
+          { by rewrite subnKC //; apply/andP; split. }
+          move: SCHEDHP => [j_hp [ARRB [HP SCHEDHP]]].
+          apply/eqP; rewrite eqb0 Bool.negb_involutive.
+          have EQ: s = j_hp.
+          { by apply only_one_job_scheduled with (sched0 := sched) (t0 := t); [apply/eqP | ]. }
+            by rewrite EQ.
+          rewrite ltn_subRL in NEQ.
+          apply leq_trans with (t1 + blocking_bound); last by apply ltnW. 
+          apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
+            by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
+        }
+        { rewrite /cumulative_priority_inversion /is_priority_inversion. 
+          rewrite -[X in _ <= X]addn0 -[ppt - t1]mul1n -iter_addn -big_const_nat. 
+          rewrite leq_sum //.
+          intros t _; case: (sched t); last by done.
+            by intros s; case: higher_eq_priority.
+        }
+        { rewrite leq_subLR.
+          apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
+          rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
+        }
+      Qed.
+      
+    End PriorityInversionIsBounded.  
+
+    (** ** Response-Time Bound *)
+    (** In this section, we prove that the maximum among the solutions of the response-time 
+        bound recurrence is a response time bound for tsk. *)
+    Section ResponseTimeBound.
+
+      (* Let L be any positive fixed point of the busy interval recurrence. *)
+      Variable L: time.
+      Hypothesis H_L_positive: L > 0.
+      Hypothesis H_fixed_point: L = blocking_bound + total_rbf L.
+
+      (* To reduce the time complexity of the analysis, recall the notion of search space. *)
+      Let is_in_search_space A :=
+        (A < L)
+          && ((task_rbf A != task_rbf (A + ε))
+           || has (fun tsko =>
+                    (tsk != tsko) && (rbf tsko (A + D tsk - D tsko)
+                                      != rbf tsko ((A + ε) + D tsk - D tsko))) ts). 
+      
+      (* Next, consider any value R, and assume that for any given arrival A from search space
+         there is a solution of the response-time bound recurrence which is bounded by R. *)
+      Variable R: nat.
+      Hypothesis H_R_is_maximum:
+        forall A,
+          is_in_search_space A -> 
+          exists  F,
+            A + F = blocking_bound
+                    + (task_rbf (A + ε) - (task_cost tsk - task_lock_in_service tsk))
+                    + W A (A + F) /\
+            F + (task_cost tsk - task_lock_in_service tsk) <= R.
+
+      (* Then, using the results for the general RTA for EDF-schedulers, we establish a 
+         response-time bound for the more concrete model of bounded nonpreemptive segments. *)
+      Theorem uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments:
+        response_time_bounded_by tsk R.
+      Proof.
+        eapply uniprocessor_response_time_bound_edf; eauto 2.
+          by apply priority_inversion_is_bounded. 
+      Qed.
+      
+    End ResponseTimeBound.
+      
+  End Analysis. 
+   
+End RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
\ No newline at end of file