Clarify definitions and comments

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\

analysis/uni/susp/dynamic/oblivious/fp_rta.v

@@ -15,7 +15,10 @@ Module SuspensionObliviousFP.
   Export ResponseTimeIterationFP ReductionToBasicSchedule.
 
   (* In this section, we formalize the suspension-oblivious RTA
-     for fixed-priority tasks under the dynamic self-suspension model. *)
+     for fixed-priority tasks under the dynamic self-suspension model.
+     This is just a straightforward application of the reduction
+     in analysis/uni/susp/dynamic/oblivious/reduction.v with the basic
+     response-time 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 suspension-aware 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 suspension-aware schedule... *)
+      Variable sched: schedule arr_seq.
 
-    (* Also assume that the schedule is work-conserving when there are non-suspended 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 work-conserving when there are non-suspended 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 response-time 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 suspension-oblivious schedulability test suceeds... *)
+      (* Then, we prove that if this suspension-oblivious response-time analysis suceeds... *)
       Hypothesis H_claimed_schedulable_by_suspension_oblivious_RTA:
         claimed_to_be_schedulable ts.
 

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.
 

model/uni/susp/last_execution.v

+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