diff git a/Makefile b/Makefile
index 3a828e16c87ad2c86f43488aeaa85eccf7915e2d..60091b87ff25e6254715567d4f775abfbea0e006 100644
 a/Makefile
+++ b/Makefile
@@ 14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/step_function.v ./util/minmax.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/uni/susp/dynamic/oblivious/fp_rta.v ./analysis/uni/susp/dynamic/oblivious/reduction.v ./analysis/uni/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/arrival_sequence.v ./model/task.v ./model/task_arrival.v ./model/suspension.v ./model/partitioned/schedulability.v ./model/partitioned/schedule.v ./model/priority.v ./model/global/workload.v ./model/global/schedulability.v ./model/global/jitter/interference_edf.v ./model/global/jitter/interference.v ./model/global/jitter/job.v ./model/global/jitter/constrained_deadlines.v ./model/global/jitter/schedule.v ./model/global/jitter/platform.v ./model/global/response_time.v ./model/global/basic/interference_edf.v ./model/global/basic/interference.v ./model/global/basic/constrained_deadlines.v ./model/global/basic/schedule.v ./model/global/basic/platform.v ./model/job.v ./model/time.v ./model/arrival_bounds.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/affinity.v ./model/apa/constrained_deadlines.v ./model/apa/platform.v ./model/uni/workload.v ./model/uni/transformation/construction.v ./model/uni/susp/suspension_intervals.v ./model/uni/susp/schedule.v ./model/uni/susp/platform.v ./model/uni/schedulability.v ./model/uni/schedule_of_task.v ./model/uni/response_time.v ./model/uni/schedule.v ./model/uni/basic/arrival_bounds.v ./model/uni/basic/busy_interval.v ./model/uni/basic/platform.v ./model/uni/service.v ./implementation/arrival_sequence.v ./implementation/task.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/job.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v ./implementation/uni/susp/dynamic/arrival_sequence.v ./implementation/uni/susp/dynamic/task.v ./implementation/uni/susp/dynamic/job.v ./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v ./implementation/uni/susp/schedule.v ./implementation/uni/basic/fp_rta_example.v ./implementation/uni/basic/schedule.v o Makefile
+# coq_makefile f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/step_function.v ./util/minmax.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/uni/susp/dynamic/oblivious/fp_rta.v ./analysis/uni/susp/dynamic/oblivious/reduction.v ./analysis/uni/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/arrival_sequence.v ./model/task.v ./model/task_arrival.v ./model/suspension.v ./model/partitioned/schedulability.v ./model/partitioned/schedule.v ./model/priority.v ./model/global/workload.v ./model/global/schedulability.v ./model/global/jitter/interference_edf.v ./model/global/jitter/interference.v ./model/global/jitter/job.v ./model/global/jitter/constrained_deadlines.v ./model/global/jitter/schedule.v ./model/global/jitter/platform.v ./model/global/response_time.v ./model/global/basic/interference_edf.v ./model/global/basic/interference.v ./model/global/basic/constrained_deadlines.v ./model/global/basic/schedule.v ./model/global/basic/platform.v ./model/job.v ./model/time.v ./model/arrival_bounds.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/affinity.v ./model/apa/constrained_deadlines.v ./model/apa/platform.v ./model/uni/workload.v ./model/uni/transformation/construction.v ./model/uni/susp/suspension_intervals.v ./model/uni/susp/last_execution.v ./model/uni/susp/schedule.v ./model/uni/susp/platform.v ./model/uni/schedulability.v ./model/uni/schedule_of_task.v ./model/uni/response_time.v ./model/uni/schedule.v ./model/uni/basic/arrival_bounds.v ./model/uni/basic/busy_interval.v ./model/uni/basic/platform.v ./model/uni/service.v ./implementation/arrival_sequence.v ./implementation/task.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/job.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v ./implementation/uni/susp/dynamic/arrival_sequence.v ./implementation/uni/susp/dynamic/task.v ./implementation/uni/susp/dynamic/job.v ./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v ./implementation/uni/susp/schedule.v ./implementation/uni/basic/fp_rta_example.v ./implementation/uni/basic/schedule.v o Makefile
#
.DEFAULT_GOAL := all
@@ 182,6 +182,7 @@ VFILES:=util/ssromega.v\
model/uni/workload.v\
model/uni/transformation/construction.v\
model/uni/susp/suspension_intervals.v\
+ model/uni/susp/last_execution.v\
model/uni/susp/schedule.v\
model/uni/susp/platform.v\
model/uni/schedulability.v\
diff git a/analysis/uni/susp/dynamic/oblivious/fp_rta.v b/analysis/uni/susp/dynamic/oblivious/fp_rta.v
index 3765496bc1f00a5510ee294a3dc9ae4501e8ece9..cfb65b04a6aeb60fbae9cb2ce520aca782184fc8 100644
 a/analysis/uni/susp/dynamic/oblivious/fp_rta.v
+++ b/analysis/uni/susp/dynamic/oblivious/fp_rta.v
@@ 15,7 +15,10 @@ Module SuspensionObliviousFP.
Export ResponseTimeIterationFP ReductionToBasicSchedule.
(* In this section, we formalize the suspensionoblivious RTA
 for fixedpriority tasks under the dynamic selfsuspension model. *)
+ for fixedpriority tasks under the dynamic selfsuspension model.
+ This is just a straightforward application of the reduction
+ in analysis/uni/susp/dynamic/oblivious/reduction.v with the basic
+ responsetime analysis for uniprocessor FP scheduling. *)
Section ReductionToBasicAnalysis.
Context {SporadicTask: eqType}.
@@ 64,48 +67,48 @@ Module SuspensionObliviousFP.
Hypothesis H_dynamic_suspensions:
dynamic_suspension_model job_cost job_task next_suspension task_suspension_bound.
 (* Next, consider any suspensionaware schedule... *)
 Variable sched: schedule arr_seq.
+ (* As part of the analysis, we are going to use task costs inflated with suspension bounds, ... *)
+ Let inflated_cost := inflated_task_cost task_cost task_suspension_bound.
 (* ...where jobs only execute after they arrive... *)
 Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
+ (* ...with the condition that they are no larger than the deadline nor the period of each task. *)
+ Hypothesis H_inflated_cost_le_deadline_and_period:
+ forall tsk,
+ tsk \in ts >
+ inflated_cost tsk <= task_deadline tsk /\
+ inflated_cost tsk <= task_period tsk.
+
+ (* Now we proceed with the schedulability analysis. *)
+ Section MainProof.
 (* ...and no longer than their execution costs. *)
 Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+ (* Consider any suspensionaware schedule... *)
+ Variable sched: schedule arr_seq.
 (* Also assume that the schedule is workconserving when there are nonsuspended jobs, ... *)
 Hypothesis H_work_conserving: work_conserving job_cost next_suspension sched.
+ (* ...where jobs only execute after they arrive... *)
+ Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
 (* ...that the schedule respects job priority... *)
 Hypothesis H_respects_priority:
 respects_FP_policy job_cost job_task next_suspension sched higher_eq_priority.
+ (* ...and no longer than their execution costs. *)
+ Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
 (* ...and that suspended jobs are not allowed to be scheduled. *)
 Hypothesis H_respects_self_suspensions:
 respects_self_suspensions job_cost next_suspension sched.
+ (* Also assume that the schedule is workconserving when there are nonsuspended jobs, ... *)
+ Hypothesis H_work_conserving: work_conserving job_cost next_suspension sched.
 (* Now we move to the schedulability analysis. *)
 Section MainProof.
+ (* ...that the schedule respects job priority... *)
+ Hypothesis H_respects_priority:
+ respects_FP_policy job_cost job_task next_suspension sched higher_eq_priority.
 (* For simplicity, let's first define some local names. *)
 Let task_is_schedulable := task_misses_no_deadline job_cost job_deadline job_task sched.

 (* Now, consider the task costs inflated with suspension bounds... *)
 Let inflated_cost := inflated_task_cost task_cost task_suspension_bound.
+ (* ...and that suspended jobs are not allowed to be scheduled. *)
+ Hypothesis H_respects_self_suspensions:
+ respects_self_suspensions job_cost next_suspension sched.
 (* ...and assume that these costs are no larger than the deadline nor the period of each task. *)
 Hypothesis H_inflated_cost_le_deadline_and_period:
 forall tsk,
 tsk \in ts >
 inflated_cost tsk <= task_deadline tsk /\
 inflated_cost tsk <= task_period tsk.
+ (* For simplicity, let's also define some local names. *)
+ Let task_is_schedulable := task_misses_no_deadline job_cost job_deadline job_task sched.
(* Next, recall the responsetime analysis for FP scheduling instantiated with
 these inflated task costs. *)
+ the inflated task costs. *)
Let claimed_to_be_schedulable :=
fp_schedulable inflated_cost task_period task_deadline higher_eq_priority.
 (* Finally, we prove that if the suspensionoblivious schedulability test suceeds... *)
+ (* Then, we prove that if this suspensionoblivious responsetime analysis suceeds... *)
Hypothesis H_claimed_schedulable_by_suspension_oblivious_RTA:
claimed_to_be_schedulable ts.
diff git a/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v b/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
index 38c3a9ddb593d3793176d996ce4747c45ce80bd5..a568e549252056950102726da0338637d28f449b 100644
 a/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
+++ b/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
@@ 166,7 +166,7 @@ Module ResponseTimeAnalysisFP.
 by apply RM_is_reflexive.
 by apply RM_is_transitive.
 by intros tsk_a tsk_b INa INb; apply/orP; apply leq_total.

+  by apply inflated_cost_le_deadline_and_period.
 by apply scheduler_jobs_must_arrive_to_execute.
 by apply scheduler_completed_jobs_dont_execute; intro j'; specialize (VALID j'); des.
 by apply scheduler_work_conserving.
@@ 174,7 +174,6 @@ Module ResponseTimeAnalysisFP.
 by intros t; apply RM_is_transitive.
 by intros _ j1 j2; apply leq_total.
 by apply scheduler_respects_self_suspensions.
  by apply inflated_cost_le_deadline_and_period.
 by apply schedulability_test_succeeds.
Qed.
diff git a/model/uni/susp/last_execution.v b/model/uni/susp/last_execution.v
new file mode 100644
index 0000000000000000000000000000000000000000..a063af8db797419a7373cc4262bb620b81587e24
 /dev/null
+++ b/model/uni/susp/last_execution.v
@@ 0,0 +1,364 @@
+Require Import rt.util.all.
+Require Import rt.model.job rt.model.arrival_sequence.
+Require Import rt.model.uni.schedule.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* In this file, we show how to compute the time instant after the last
+ execution of a job and prove several lemmas about that instant. This
+ notion is crucial for defining suspension intervals. *)
+Module LastExecution.
+
+ Export Job UniprocessorSchedule.
+
+ (* In this section we define the time after the last execution of a job (if exists). *)
+ Section TimeAfterLastExecution.
+
+ Context {Job: eqType}.
+ Variable job_cost: Job > time.
+
+ (* Consider any uniprocessor schedule. *)
+ Context {arr_seq: arrival_sequence Job}.
+ Variable sched: schedule arr_seq.
+
+ (* For simplicity, let's define some local names. *)
+ Let job_scheduled_at := scheduled_at sched.
+ Let job_completed_by := completed_by job_cost sched.
+
+ Section Defs.
+
+ (* Let j be any job in the arrival sequence. *)
+ Variable j: JobIn arr_seq.
+
+ (* Next, we will show how to find the time after the most recent
+ execution of a given job j in the interval [job_arrival j, t).
+ (Note that this instant can be time t itself.) *)
+ Variable t: time.
+
+ (* Let scheduled_before denote whether job j was scheduled in the interval [0, t). *)
+ Let scheduled_before :=
+ [exists t0: 'I_t, job_scheduled_at j t0].
+
+ (* In case j was scheduled before, we define the last time in which j was scheduled. *)
+ Let last_time_scheduled :=
+ \max_(t_last < t  job_scheduled_at j t_last) t_last.
+
+ (* Then, the time after the last execution of job j in the interval [0, t), if exists,
+ occurs:
+ (a) immediately after the last time in which job j was scheduled, or,
+ (b) if j was never scheduled, at the arrival time of j. *)
+ Definition time_after_last_execution :=
+ if scheduled_before then
+ last_time_scheduled + 1
+ else job_arrival j.
+
+ End Defs.
+
+ (* Next, we prove lemmas about the time after the last execution. *)
+ Section Lemmas.
+
+ (* Assume that jobs do not execute before they arrived. *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* Let j be any job in the arrival sequence. *)
+ Variable j: JobIn arr_seq.
+
+ (* In this section, we show that the time after the last execution occurs
+ no earlier than the arrival of the job. *)
+ Section JobHasArrived.
+
+ (* Then, the time following the last execution of job j in the
+ interval [0, t) occurs no earlier than the arrival of j. *)
+ Lemma last_execution_after_arrival:
+ forall t,
+ has_arrived j (time_after_last_execution j t).
+ Proof.
+ unfold time_after_last_execution, has_arrived; intros t.
+ case EX: [exists _, _]; last by done.
+ move: EX => /existsP [t0 SCHED].
+ apply leq_trans with (n := t0 + 1);
+ last by rewrite leq_add2r; apply leq_bigmax_cond.
+ apply leq_trans with (n := t0); last by rewrite addn1.
+ by apply H_jobs_must_arrive_to_execute.
+ Qed.
+
+ End JobHasArrived.
+
+ (* Next, we establish the monotonicity of the function. *)
+ Section Monotonicity.
+
+ (* Let t1 be any time no earlier than the arrival of job j. *)
+ Variable t1: time.
+ Hypothesis H_after_arrival: has_arrived j t1.
+
+ (* Then, (time_after_last_execution j) grows monotonically
+ after that point. *)
+ Lemma last_execution_monotonic:
+ forall t2,
+ t1 <= t2 >
+ time_after_last_execution j t1 <= time_after_last_execution j t2.
+ Proof.
+ rename H_jobs_must_arrive_to_execute into ARR.
+ intros t2 LE12.
+ rewrite /time_after_last_execution.
+ case EX1: [exists _, _].
+ {
+ move: EX1 => /existsP [t0 SCHED0].
+ have EX2: [exists t:'I_t2, job_scheduled_at j t].
+ {
+ have LT: t0 < t2 by apply: (leq_trans _ LE12).
+ by apply/existsP; exists (Ordinal LT).
+ }
+ rewrite EX2 2!addn1.
+ set m1 := \max_(_ < t1  _)_.
+ have LTm1: m1 < t2.
+ {
+ apply: (leq_trans _ LE12).
+ by apply bigmax_ltn_ord with (i0 := t0).
+ }
+ apply leq_ltn_trans with (n := Ordinal LTm1); first by done.
+ by apply leq_bigmax_cond, (bigmax_pred _ _ t0).
+ }
+ {
+ case EX2: [exists _, _]; last by done.
+ move: EX2 => /existsP [t0 SCHED0].
+ set m2 := \max_(_ < t2  _)_.
+ rewrite addn1 ltnW // ltnS.
+ have SCHED2: scheduled_at sched j m2 by apply (bigmax_pred _ _ t0).
+ by apply ARR in SCHED2.
+ }
+ Qed.
+
+ End Monotonicity.
+
+ (* Next, we prove that the function is idempotent. *)
+ Section Idempotence.
+
+ (* The time after the last execution of job j is an idempotent function. *)
+ Lemma last_execution_idempotent:
+ forall t,
+ time_after_last_execution j (time_after_last_execution j t)
+ = time_after_last_execution j t.
+ Proof.
+ rename H_jobs_must_arrive_to_execute into ARR.
+ intros t.
+ rewrite {2 3}/time_after_last_execution.
+ case EX: [exists _,_].
+ {
+ move: EX => /existsP [t0 SCHED].
+ rewrite /time_after_last_execution.
+ set ex := [exists t0, _].
+ have EX': ex.
+ {
+ apply/existsP; rewrite addn1.
+ exists (Ordinal (ltnSn _)).
+ by apply bigmax_pred with (i0 := t0).
+ }
+ rewrite EX'; f_equal.
+ rewrite addn1; apply/eqP.
+ set m := \max_(_ < t  _)_.
+ have LT: m < m.+1 by done.
+ rewrite eqn_leq; apply/andP; split.
+ {
+ rewrite ltnS; apply bigmax_ltn_ord with (i0 := Ordinal LT).
+ by apply bigmax_pred with (i0 := t0).
+ }
+ {
+ apply leq_trans with (n := Ordinal LT); first by done.
+ by apply leq_bigmax_cond, bigmax_pred with (i0 := t0).
+ }
+ }
+ {
+ apply negbT in EX; rewrite negb_exists in EX.
+ move: EX => /forallP EX.
+ rewrite /time_after_last_execution.
+ set ex := [exists _, _].
+ suff EX': ex = false; first by rewrite EX'.
+ apply negbTE; rewrite negb_exists; apply/forallP.
+ intros x.
+ apply/negP; intro SCHED.
+ apply ARR in SCHED.
+ by apply leq_ltn_trans with (p := job_arrival j) in SCHED;
+ first by rewrite ltnn in SCHED.
+ }
+ Qed.
+
+ End Idempotence.
+
+ (* Next, we show that time_after_last_execution is bounded by the identity function. *)
+ Section BoundedByIdentity.
+
+ (* Let t be any time no earlier than the arrival of j. *)
+ Variable t: time.
+ Hypothesis H_after_arrival: has_arrived j t.
+
+ (* Then, the time following the last execution of job j in the interval [0, t)
+ occurs no later than time t. *)
+ Lemma last_execution_bounded_by_identity:
+ time_after_last_execution j t <= t.
+ Proof.
+ unfold time_after_last_execution.
+ case EX: [exists _, _]; last by done.
+ move: EX => /existsP [t0 SCHED].
+ by rewrite addn1; apply bigmax_ltn_ord with (i0 := t0).
+ Qed.
+
+ End BoundedByIdentity.
+
+ (* In this section, we show that if the service received by a job
+ remains the same, the time after last execution also doesn't change. *)
+ Section SameLastExecution.
+
+ (* Consider any time instants t and t'... *)
+ Variable t t': time.
+
+ (* ...in which job j has received the same amount of service. *)
+ Hypothesis H_same_service: service sched j t = service sched j t'.
+
+ (* Then, we prove that the times after last execution relative to
+ instants t and t' are exactly the same. *)
+ Lemma same_service_implies_same_last_execution:
+ time_after_last_execution j t = time_after_last_execution j t'.
+ Proof.
+ rename H_same_service into SERV.
+ have IFF := same_service_implies_scheduled_at_earlier_times
+ sched j t t' SERV.
+ rewrite /time_after_last_execution.
+ rewrite IFF; case EX2: [exists _, _]; [f_equal  by done].
+ have EX1: [exists x: 'I_t, job_scheduled_at j x] by rewrite IFF.
+ clear IFF.
+ move: t t' SERV EX1 EX2 => t1 t2; clear t t'.
+ wlog: t1 t2 / t1 <= t2 => [EQ SERV EX1 EX2  LE].
+ by case/orP: (leq_total t1 t2); ins; [symmetry]; apply EQ.
+
+ set m1 := \max_(t < t1  job_scheduled_at j t) t.
+ set m2 := \max_(t < t2  job_scheduled_at j t) t.
+ move => SERV /existsP [t1' SCHED1'] /existsP [t2' SCHED2'].
+ apply/eqP; rewrite eqn_leq; apply/andP; split.
+ {
+ have WID := big_ord_widen_cond t2
+ (fun x => job_scheduled_at j x) (fun x => x).
+ rewrite /m1 /m2 {}WID //.
+ rewrite big_mkcond [\max_(t < t2  _) _]big_mkcond.
+ apply leq_big_max; intros i _.
+ case AND: (_ && _); last by done.
+ by move: AND => /andP [SCHED _]; rewrite SCHED.
+ }
+ {
+ destruct (leqP t2 m1) as [GEm1  LTm1].
+ {
+ apply leq_trans with (n := t2); last by done.
+ by apply ltnW, bigmax_ltn_ord with (i0 := t2').
+ }
+ destruct (ltnP m2 t1) as [LTm2  GEm2].
+ {
+ apply leq_trans with (n := Ordinal LTm2); first by done.
+ by apply leq_bigmax_cond, bigmax_pred with (i0 := t2').
+ }
+ have LTm2: m2 < t2 by apply bigmax_ltn_ord with (i0 := t2').
+ have SCHEDm2: job_scheduled_at j m2 by apply bigmax_pred with (i0 := t2').
+ exfalso; move: SERV => /eqP SERV.
+ rewrite [_ == _]negbK in SERV.
+ move: SERV => /negP SERV; apply SERV; clear SERV.
+ rewrite neq_ltn; apply/orP; left.
+ rewrite /service /service_during.
+ rewrite > big_cat_nat with (n := m2) (p := t2);
+ [simpl  by done  by apply ltnW].
+ rewrite addn1; apply leq_add; first by apply extend_sum.
+ destruct t2; first by rewrite ltn0 in LTm1.
+ rewrite big_nat_recl; last by done.
+ by rewrite /service_at /job_scheduled_at SCHEDm2.
+ }
+ Qed.
+
+ End SameLastExecution.
+
+ (* In this section, we show that the service received by a job
+ does not change since the last execution. *)
+ Section SameService.
+
+ (* We prove that, for any time t, the service received by job j
+ before (time_after_last_execution j t) is the same as the service
+ by j before time t. *)
+ Lemma same_service_since_last_execution:
+ forall t,
+ service sched j (time_after_last_execution j t) = service sched j t.
+ Proof.
+ intros t; rewrite /time_after_last_execution.
+ case EX: [exists _, _].
+ {
+ move: EX => /existsP [t0 SCHED0].
+ set m := \max_(_ < _  _) _; rewrite addn1.
+ have LTt: m < t by apply: (bigmax_ltn_ord _ _ t0).
+ rewrite leq_eqVlt in LTt.
+ move: LTt => /orP [/eqP EQ  LTt]; first by rewrite EQ.
+ rewrite {2}/service/service_during.
+ rewrite > big_cat_nat with (n := m.+1);
+ [simpl  by done  by apply ltnW].
+ rewrite [X in _ + X]big_nat_cond [X in _ + X]big1 ?addn0 //.
+ move => i /andP [/andP [GTi LTi] _].
+ apply/eqP; rewrite eqb0; apply/negP; intro BUG.
+ have LEi: (Ordinal LTi) <= m by apply leq_bigmax_cond.
+ by apply (leq_ltn_trans LEi) in GTi; rewrite ltnn in GTi.
+ }
+ {
+ apply negbT in EX; rewrite negb_exists in EX.
+ move: EX => /forallP ALL.
+ rewrite /service /service_during.
+ rewrite ignore_service_before_arrival // big_geq //.
+ rewrite big_nat_cond big1 //; move => i /andP [/= LTi _].
+ by apply/eqP; rewrite eqb0; apply (ALL (Ordinal LTi)).
+ }
+ Qed.
+
+ End SameService.
+
+ (* In this section, we show that for any smaller value of service, we can
+ always find the last execution that corresponds to that service. *)
+ Section ExistsIntermediateExecution.
+
+ (* Assume that job j has completed by time t. *)
+ Variable t: time.
+ Hypothesis H_j_has_completed: completed_by job_cost sched j t.
+
+ (* Then, for any value of service less than the cost of j, ...*)
+ Variable s: time.
+ Hypothesis H_less_than_cost: s < job_cost j.
+
+ (* ...there exists a last execution where the service received
+ by job j equals s. *)
+ Lemma exists_last_execution_with_smaller_service:
+ exists t0,
+ service sched j (time_after_last_execution j t0) = s.
+ Proof.
+ have SAME := same_service_since_last_execution.
+ rename H_jobs_must_arrive_to_execute into ARR.
+ move: H_j_has_completed => /eqP COMP.
+ feed (exists_intermediate_point (service sched j));
+ first by apply service_is_a_step_function.
+ move => EX; feed (EX (job_arrival j) t).
+ {
+ feed (cumulative_service_implies_scheduled sched j 0 t);
+ first by apply leq_ltn_trans with (n := s);
+ last by rewrite /(service _ _ _) COMP.
+ move => [t' [/= LTt SCHED]].
+ apply leq_trans with (n := t'); last by apply ltnW.
+ by apply ARR in SCHED.
+ }
+ feed (EX s).
+ {
+ apply/andP; split; last by rewrite COMP.
+ rewrite /service /service_during.
+ by rewrite ignore_service_before_arrival // big_geq.
+ }
+ move: EX => [x_mid [_ SERV]]; exists x_mid.
+ by rewrite SERV SAME.
+ Qed.
+
+ End ExistsIntermediateExecution.
+
+ End Lemmas.
+
+ End TimeAfterLastExecution.
+
+End LastExecution.
\ No newline at end of file
diff git a/model/uni/susp/suspension_intervals.v b/model/uni/susp/suspension_intervals.v
index fdb361b1796c8e9f9d098baa8909f0a9909808a0..dd4d18102fc1eaf6edebbe69521ae8095762e70b 100644
 a/model/uni/susp/suspension_intervals.v
+++ b/model/uni/susp/suspension_intervals.v
@@ 1,11 +1,12 @@
Require Import rt.util.all.
Require Import rt.model.job rt.model.arrival_sequence rt.model.suspension.
Require Import rt.model.uni.schedule.
+Require Import rt.model.uni.susp.last_execution.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module SuspensionIntervals.
 Export Job UniprocessorSchedule Suspension.
+ Export Job UniprocessorSchedule Suspension LastExecution.
(* In this section we define job suspension intervals in a schedule. *)
Section DefiningSuspensionIntervals.
@@ 24,366 +25,8 @@ Module SuspensionIntervals.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
 (* In this section, we define when jobs may begin to suspend. *)
 Section BeginningOfSuspension.

 Section Defs.

 (* Let j be any job in the arrival sequence. *)
 Variable j: JobIn arr_seq.

 (* Next, we will show how to find the most recent selfsuspension
 incurred by job j in the interval [0, t], if exists.
 As we will show next, that corresponds to the time after the most
 recent execution of job in the interval [0, t). *)
 Variable t: time.

 (* Let scheduled_before denote whether job j was scheduled in the interval [0, t). *)
 Let scheduled_before :=
 [exists t0: 'I_t, job_scheduled_at j t0].

 (* In case j was scheduled before, we define the last time in which j was scheduled. *)
 Let last_time_scheduled :=
 \max_(t_last < t  job_scheduled_at j t_last) t_last.

 (* Then, the most recent selfsuspension of job j in the interval [0, t], if exists,
 occurs:
 (a) immediately after the last time in which job j was scheduled, or,
 (b) if j was never scheduled, at the arrival time of j. *)
 Definition time_after_last_execution :=
 if scheduled_before then
 last_time_scheduled + 1
 else job_arrival j.

 End Defs.

 (* Next, we prove lemmas about the time following the last execution. *)
 Section Lemmas.

 (* Let j be any job in the arrival sequence. *)
 Variable j: JobIn arr_seq.

 (* In this section, we show that the time after the last execution occurs
 no earlier than the arrival of the job. *)
 Section JobHasArrived.

 (* Assume that jobs do not execute before they arrived. *)
 Hypothesis H_jobs_must_arrive_to_execute:
 jobs_must_arrive_to_execute sched.

 (* Then, the time following the last execution of job j in the
 interval [0, t) occurs no earlier than the arrival of j. *)
 Lemma last_execution_after_arrival:
 forall t,
 has_arrived j (time_after_last_execution j t).
 Proof.
 unfold time_after_last_execution, has_arrived; intros t.
 case EX: [exists _, _]; last by done.
 move: EX => /existsP [t0 SCHED].
 apply leq_trans with (n := t0 + 1);
 last by rewrite leq_add2r; apply leq_bigmax_cond.
 apply leq_trans with (n := t0); last by rewrite addn1.
 by apply H_jobs_must_arrive_to_execute.
 Qed.

 End JobHasArrived.

 (* Next, we establish the monotonicity of the function. *)
 Section Monotonicity.

 (* Assume that jobs do not execute before they arrived. *)
 Hypothesis H_jobs_must_arrive_to_execute:
 jobs_must_arrive_to_execute sched.

 (* Let t1 be any time no earlier than the arrival of job j. *)
 Variable t1: time.
 Hypothesis H_after_arrival: has_arrived j t1.

 (* Then, (time_after_last_execution j) grows monotonically
 after that point. *)
 Lemma last_execution_monotonic:
 forall t2,
 t1 <= t2 >
 time_after_last_execution j t1 <= time_after_last_execution j t2.
 Proof.
 rename H_jobs_must_arrive_to_execute into ARR.
 intros t2 LE12.
 rewrite /time_after_last_execution.
 case EX1: [exists _, _].
 {
 move: EX1 => /existsP [t0 SCHED0].
 have EX2: [exists t:'I_t2, job_scheduled_at j t].
 {
 have LT: t0 < t2 by apply: (leq_trans _ LE12).
 by apply/existsP; exists (Ordinal LT).
 }
 rewrite EX2 2!addn1.
 set m1 := \max_(_ < t1  _)_.
 have LTm1: m1 < t2.
 {
 apply: (leq_trans _ LE12).
 by apply bigmax_ltn_ord with (i0 := t0).
 }
 apply leq_ltn_trans with (n := Ordinal LTm1); first by done.
 by apply leq_bigmax_cond, (bigmax_pred _ _ t0).
 }
 {
 case EX2: [exists _, _]; last by done.
 move: EX2 => /existsP [t0 SCHED0].
 set m2 := \max_(_ < t2  _)_.
 rewrite addn1 ltnW // ltnS.
 have SCHED2: scheduled_at sched j m2 by apply (bigmax_pred _ _ t0).
 by apply ARR in SCHED2.
 }
 Qed.

 End Monotonicity.

 (* Next, we prove that the function is idempotent. *)
 Section Idempotence.

 (* Assume that jobs do not execute before they arrived. *)
 Hypothesis H_jobs_must_arrive_to_execute:
 jobs_must_arrive_to_execute sched.

 (* Then, we prove that the time following the last execution of
 job j is an idempotent function. *)
 Lemma last_execution_idempotent:
 forall t,
 time_after_last_execution j (time_after_last_execution j t)
 = time_after_last_execution j t.
 Proof.
 rename H_jobs_must_arrive_to_execute into ARR.
 intros t.
 rewrite {2 3}/time_after_last_execution.
 case EX: [exists _,_].
 {
 move: EX => /existsP [t0 SCHED].
 rewrite /time_after_last_execution.
 set ex := [exists t0, _].
 have EX': ex.
 {
 apply/existsP; rewrite addn1.
 exists (Ordinal (ltnSn _)).
 by apply bigmax_pred with (i0 := t0).
 }
 rewrite EX'; f_equal.
 rewrite addn1; apply/eqP.
 set m := \max_(_ < t  _)_.
 have LT: m < m.+1 by done.
 rewrite eqn_leq; apply/andP; split.
 {
 rewrite ltnS; apply bigmax_ltn_ord with (i0 := Ordinal LT).
 by apply bigmax_pred with (i0 := t0).
 }
 {
 apply leq_trans with (n := Ordinal LT); first by done.
 by apply leq_bigmax_cond, bigmax_pred with (i0 := t0).
 }
 }
 {
 apply negbT in EX; rewrite negb_exists in EX.
 move: EX => /forallP EX.
 rewrite /time_after_last_execution.
 set ex := [exists _, _].
 suff EX': ex = false; first by rewrite EX'.
 apply negbTE; rewrite negb_exists; apply/forallP.
 intros x.
 apply/negP; intro SCHED.
 apply ARR in SCHED.
 by apply leq_ltn_trans with (p := job_arrival j) in SCHED;
 first by rewrite ltnn in SCHED.
 }
 Qed.

 End Idempotence.

 (* Next, we show that time_after_last_execution is bounded by the identity function. *)
 Section BoundedByIdentity.

 (* Let t be any time no earlier than the arrival of j. *)
 Variable t: time.
 Hypothesis H_after_arrival: has_arrived j t.

 (* Then, the time following the last execution of job j in the interval [0, t)
 occurs no later than time t. *)
 Lemma last_execution_bounded_by_identity:
 time_after_last_execution j t <= t.
 Proof.
 unfold time_after_last_execution.
 case EX: [exists _, _]; last by done.
 move: EX => /existsP [t0 SCHED].
 by rewrite addn1; apply bigmax_ltn_ord with (i0 := t0).
 Qed.

 End BoundedByIdentity.

 (* In this section, we show that if the service received by a job
 remains the same, the time after last execution also doesn't change. *)
 Section SameLastExecution.

 (* Consider any time instants t and t'... *)
 Variable t t': time.

 (* ...in which job j has received the same amount of service. *)
 Hypothesis H_same_service: service sched j t = service sched j t'.

 (* Then, we prove that the times after last execution relative to
 instants t and t' are exactly the same. *)
 Lemma same_service_implies_same_last_execution:
 time_after_last_execution j t = time_after_last_execution j t'.
 Proof.
 rename H_same_service into SERV.
 have IFF := same_service_implies_scheduled_at_earlier_times
 sched j t t' SERV.
 rewrite /time_after_last_execution.
 rewrite IFF; case EX2: [exists _, _]; [f_equal  by done].
 have EX1: [exists x: 'I_t, job_scheduled_at j x] by rewrite IFF.
 clear IFF.
 move: t t' SERV EX1 EX2 => t1 t2; clear t t'.
 wlog: t1 t2 / t1 <= t2 => [EQ SERV EX1 EX2  LE].
 by case/orP: (leq_total t1 t2); ins; [symmetry]; apply EQ.

 set m1 := \max_(t < t1  job_scheduled_at j t) t.
 set m2 := \max_(t < t2  job_scheduled_at j t) t.
 move => SERV /existsP [t1' SCHED1'] /existsP [t2' SCHED2'].
 apply/eqP; rewrite eqn_leq; apply/andP; split.
 {
 have WID := big_ord_widen_cond t2
 (fun x => job_scheduled_at j x) (fun x => x).
 rewrite /m1 /m2 {}WID //.
 rewrite big_mkcond [\max_(t < t2  _) _]big_mkcond.
 apply leq_big_max; intros i _.
 case AND: (_ && _); last by done.
 by move: AND => /andP [SCHED _]; rewrite SCHED.
 }
 {
 destruct (leqP t2 m1) as [GEm1  LTm1].
 {
 apply leq_trans with (n := t2); last by done.
 by apply ltnW, bigmax_ltn_ord with (i0 := t2').
 }
 destruct (ltnP m2 t1) as [LTm2  GEm2].
 {
 apply leq_trans with (n := Ordinal LTm2); first by done.
 by apply leq_bigmax_cond, bigmax_pred with (i0 := t2').
 }
 have LTm2: m2 < t2 by apply bigmax_ltn_ord with (i0 := t2').
 have SCHEDm2: job_scheduled_at j m2 by apply bigmax_pred with (i0 := t2').
 exfalso; move: SERV => /eqP SERV.
 rewrite [_ == _]negbK in SERV.
 move: SERV => /negP SERV; apply SERV; clear SERV.
 rewrite neq_ltn; apply/orP; left.
 rewrite /service /service_during.
 rewrite > big_cat_nat with (n := m2) (p := t2);
 [simpl  by done  by apply ltnW].
 rewrite addn1; apply leq_add; first by apply extend_sum.
 destruct t2; first by rewrite ltn0 in LTm1.
 rewrite big_nat_recl; last by done.
 by rewrite /service_at /job_scheduled_at SCHEDm2.
 }
 Qed.

 End SameLastExecution.

 (* In this section, we show that the service received by a job
 does not change since the last execution. *)
 Section SameService.

 (* Assume that jobs do not execute before they arrived. *)
 Hypothesis H_jobs_must_arrive_to_execute:
 jobs_must_arrive_to_execute sched.

 (* Then, we prove that, for any time t, the service received by job j
 before (time_after_last_execution j t) is the same as the service
 by j before time t. *)
 Lemma same_service_since_last_execution:
 forall t,
 service sched j (time_after_last_execution j t) = service sched j t.
 Proof.
 intros t; rewrite /time_after_last_execution.
 case EX: [exists _, _].
 {
 move: EX => /existsP [t0 SCHED0].
 set m := \max_(_ < _  _) _; rewrite addn1.
 have LTt: m < t by apply: (bigmax_ltn_ord _ _ t0).
 rewrite leq_eqVlt in LTt.
 move: LTt => /orP [/eqP EQ  LTt]; first by rewrite EQ.
 rewrite {2}/service/service_during.
 rewrite > big_cat_nat with (n := m.+1);
 [simpl  by done  by apply ltnW].
 rewrite [X in _ + X]big_nat_cond [X in _ + X]big1 ?addn0 //.
 move => i /andP [/andP [GTi LTi] _].
 apply/eqP; rewrite eqb0; apply/negP; intro BUG.
 have LEi: (Ordinal LTi) <= m by apply leq_bigmax_cond.
 by apply (leq_ltn_trans LEi) in GTi; rewrite ltnn in GTi.
 }
 {
 apply negbT in EX; rewrite negb_exists in EX.
 move: EX => /forallP ALL.
 rewrite /service /service_during.
 rewrite ignore_service_before_arrival // big_geq //.
 rewrite big_nat_cond big1 //; move => i /andP [/= LTi _].
 by apply/eqP; rewrite eqb0; apply (ALL (Ordinal LTi)).
 }
 Qed.

 End SameService.

 (* In this section, we show that for any smaller value of service, we can
 always find the last execution that corresponds to that service. *)
 Section ExistsIntermediateExecution.

 (* Assume that jobs do not execute before they arrived. *)
 Hypothesis H_jobs_must_arrive_to_execute:
 jobs_must_arrive_to_execute sched.

 (* Assume that job j has completed by time t. *)
 Variable t: time.
 Hypothesis H_j_has_completed: completed_by job_cost sched j t.

 (* Then, for any value of service less than the cost of j, ...*)
 Variable s: time.
 Hypothesis H_less_than_cost: s < job_cost j.

 (* ...there exists a last execution where the service received
 by job j equals s. *)
 Lemma exists_last_execution_with_smaller_service:
 exists t0,
 service sched j (time_after_last_execution j t0) = s.
 Proof.
 have SAME := same_service_since_last_execution.
 rename H_jobs_must_arrive_to_execute into ARR.
 move: H_j_has_completed => /eqP COMP.
 feed (exists_intermediate_point (service sched j));
 first by apply service_is_a_step_function.
 move => EX; feed (EX (job_arrival j) t).
 {
 feed (cumulative_service_implies_scheduled sched j 0 t);
 first by apply leq_ltn_trans with (n := s);
 last by rewrite /(service _ _ _) COMP.
 move => [t' [/= LTt SCHED]].
 apply leq_trans with (n := t'); last by apply ltnW.
 by apply ARR in SCHED.
 }
 feed (EX s).
 {
 apply/andP; split; last by rewrite COMP.
 rewrite /service /service_during.
 by rewrite ignore_service_before_arrival // big_geq.
 }
 move: EX => [x_mid [_ SERV]]; exists x_mid.
 by rewrite SERV SAME.
 Qed.

 End ExistsIntermediateExecution.

 End Lemmas.

 End BeginningOfSuspension.

 (* Having identified the time after last execution, we now define
 whether jobs are suspended. *)
+ (* Based on the time after the last execution of a job, we define next
+ whether a job is suspended. *)
Section JobSuspension.
(* Let j be any job in the arrival sequence. *)
@@ 394,10 +37,10 @@ Module SuspensionIntervals.
(* We are going to define whether job j is suspended at time t. *)
Variable t: time.
 (* First, we define the (potential) begin of the latest self suspension as the
+ (* First, we define the beginning of the latest self suspension as the
time following the last execution of job j in the interval [0, t).
(Note that suspension_start can return time t itself.) *)
 Let suspension_start := time_after_last_execution j t.
+ Let suspension_start := time_after_last_execution sched j t.
(* Next, using the service received by j in the interval [0, suspension_start), ... *)
Let current_service := service sched j suspension_start.
@@ 407,7 +50,9 @@ Module SuspensionIntervals.
Definition suspension_duration := next_suspension j current_service.
(* Then, we say that job j is suspended at time t iff j has not completed
 by time t and t lies in the latest suspension interval. *)
+ by time t and t lies in the latest suspension interval.
+ (Also note that the suspension interval can have duration 0, in which
+ case suspended_at will be trivially false.) *)
Definition suspended_at :=
~~ completed_by job_cost sched j t &&
(suspension_start <= t < suspension_start + suspension_duration).
@@ 461,7 +106,7 @@ Module SuspensionIntervals.
Hypothesis H_has_arrived: has_arrived j t.
(* ...and recall the latest suspension interval of job j relative to time t. *)
 Let suspension_start := time_after_last_execution j t.
+ Let suspension_start := time_after_last_execution sched j t.
Let duration := suspension_duration j t.
(* First, we analyze the service received during a suspension interval. *)
@@ 504,7 +149,7 @@ Module SuspensionIntervals.
case: (boolP (completed_by _ _ _ _)) => [COMP  NOTCOMP];
first by apply completed_implies_not_scheduled in COMP;
first by rewrite SCHED' in COMP.
 rewrite andTb (same_service_implies_same_last_execution _ _ suspension_start) //.
+ rewrite andTb (same_service_implies_same_last_execution _ _ _ suspension_start) //.
rewrite /suspension_start last_execution_idempotent //.
apply/andP; split; first by apply leq_addr.
by rewrite ltn_add2l.
@@ 541,10 +186,10 @@ Module SuspensionIntervals.
apply/andP; split;
first by apply last_execution_bounded_by_identity.
apply (leq_trans LT).
 have SAME: time_after_last_execution j t = time_after_last_execution j t_in.
+ have SAME: time_after_last_execution sched j t = time_after_last_execution sched j t_in.
{
set b := _ _ t.
 rewrite [_ _ t_in](same_service_implies_same_last_execution _ _ b);
+ rewrite [_ _ t_in](same_service_implies_same_last_execution _ _ _ b);
first by rewrite last_execution_idempotent.
apply same_service_in_suspension_interval.
by apply/andP; split; last by apply ltnW.
@@ 662,7 +307,7 @@ Module SuspensionIntervals.
}
move: EX => /existsP [t' /andP [GE' /eqP SERV]].
unfold suspended_at, suspension_duration.
 set b := time_after_last_execution j.
+ set b := time_after_last_execution sched j.
set n := next_suspension j s.
apply leq_trans with (n := \sum_(t1 <= t < t2  b t' <= t < b t' + n) 1).
{
@@ 677,13 +322,13 @@ Module SuspensionIntervals.
move: INT => /andP [GEt LTt].
rewrite (same_service_in_suspension_interval _ _ _ _ t') //.
{
 rewrite /b [b t'](same_service_implies_same_last_execution _ _ t);
+ rewrite /b [b t'](same_service_implies_same_last_execution _ _ _ t);
last by rewrite SERV EQ.
by apply/andP; split.
}
{
rewrite /suspension_duration /b.
 rewrite [b t'](same_service_implies_same_last_execution _ _ t);
+ rewrite [b t'](same_service_implies_same_last_execution _ _ _ t);
last by rewrite SERV EQ.
by apply/andP; split; last by apply ltnW.
}
@@ 724,7 +369,7 @@ Module SuspensionIntervals.
cumulative_suspension j t = total_suspension job_cost next_suspension j.
Proof.
rename H_j_has_completed into COMP, H_jobs_must_arrive_to_execute into ARR.
 have EARLIER := exists_last_execution_with_smaller_service j ARR t COMP.
+ have EARLIER := exists_last_execution_with_smaller_service job_cost sched ARR j t COMP.
apply/eqP; rewrite eqn_leq; apply/andP; split;
first by apply cumulative_suspension_le_total_suspension.
rewrite /total_suspension /cumulative_suspension /cumulative_suspension_during.
@@ 754,12 +399,12 @@ Module SuspensionIntervals.
{
apply leq_sum_nat; move => s /andP [_ LTs] _.
rewrite /suspended_at /suspension_duration.
 set b := time_after_last_execution j.
+ set b := time_after_last_execution sched j.
set n := next_suspension j.
move: (EARLIER s LTs) => [t' EQ'].
apply leq_trans with (n := \sum_(0 <= t0 < t  (service sched j t0 == s) &&
 (b t' <= t0 < b t' + n (service sched j (b t')))) 1); last first.
+ (b t' <= t0 < b t' + n (service sched j (b t')))) 1); last first.
{
rewrite big_mkcond [\sum_(_ <= _ < _  _ == s)_]big_mkcond.
apply leq_sum_nat; move => i /andP [_ LTi] _.