Library rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.10.1 (October 2019)

----------------------------------------------------------------------------- *)

From rt.util Require Import all.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.preemption Require Import valid_model job.parameters.
From rt.restructuring.analysis.basic_facts.preemption Require Import
     rtc_threshold.job_preemptable.
From rt.restructuring.analysis.abstract Require Import core.definitions.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Run-to-Completion Threshold of a job

In this module, we provide a sufficient condition under which a job receives enough service to become nonpreemptive. Previously we defined the notion of run-to-completion threshold (see file abstract.run_to_completion_threshold.v). Run-to-completion threshold is the amount of service after which a job cannot be preempted until its completion. In this section we prove that if cumulative interference inside a busy interval is bounded by a certain constant then a job executes long enough to reach its run-to-completion threshold and become nonpreemptive.
Section AbstractRTARunToCompletionThreshold.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

In addition, we assume existence of a function maping jobs to their preemption points.
  Context `{JobPreemptable Job}.

Consider any arrival sequence with consistent arrivals...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Next, consider any ideal uniprocessor schedule of this arrival sequence.
  Variable sched : schedule (ideal.processor_state Job).

Assume that the job costs are no larger than the task costs.
  Hypothesis H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.

Let tsk be any task that is to be analyzed.
  Variable tsk : Task.

Assume we are provided with abstract functions for interference and interfering workload.
  Variable interference : Job → instant → bool.
  Variable interfering_workload : Job → instant → duration.

For simplicity, let's define some local names.
  Let work_conserving := work_conserving arr_seq sched tsk.
  Let cumul_interference := cumul_interference interference.
  Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
  Let busy_interval := busy_interval sched interference interfering_workload.

We assume that the schedule is work-conserving.
  Hypothesis H_work_conserving: work_conserving interference interfering_workload.

Let j be any job of task tsk with positive cost.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_of_tsk : job_task j = tsk.
  Hypothesis H_job_cost_positive : job_cost_positive j.

Next, consider any busy interval [t1, t2) of job j.
  Variable t1 t2 : instant.
  Hypothesis H_busy_interval : busy_interval j t1 t2.

First, we prove that job j completes by the end of the busy interval. Note that the busy interval contains the execution of job j, in addition time instant t2 is a quiet time. Thus by the definition of a quiet time the job should be completed before time t2.
  Lemma job_completes_within_busy_interval:
    completed_by sched j t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 197)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  ============================
  completed_by sched j t2

----------------------------------------------------------------------------- *)

  Proof.
    move: (H_busy_interval) ⇒ [[/andP [_ LT] [_ _]] [_ QT2]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 278)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  LT : job_arrival j < t2
  QT2 : ~~ pending_earlier_and_at sched j t2
  ============================
  completed_by sched j t2

----------------------------------------------------------------------------- *)

    unfold pending, has_arrived in QT2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 279)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  LT : job_arrival j < t2
  QT2 : ~~ pending_earlier_and_at sched j t2
  ============================
  completed_by sched j t2

----------------------------------------------------------------------------- *)

    move: QT2; rewrite /pending negb_and; move ⇒ /orP [QT2|QT2].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 335)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  LT : job_arrival j < t2
  QT2 : ~~ arrived_before j t2
  ============================
  completed_by sched j t2

subgoal 2 (ID 336) is:
 completed_by sched j t2

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 335)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  LT : job_arrival j < t2
  QT2 : ~~ arrived_before j t2
  ============================
  completed_by sched j t2

----------------------------------------------------------------------------- *)

by move: QT2 ⇒ /negP QT2; exfalso; apply QT2, ltnW.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 336)

subgoal 1 (ID 336) is:
 completed_by sched j t2

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 336)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  LT : job_arrival j < t2
  QT2 : ~~ ~~ completed_by sched j t2
  ============================
  completed_by sched j t2

----------------------------------------------------------------------------- *)

      by rewrite Bool.negb_involutive in QT2.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

In this section we show that the cumulative interference is a complement to the total time where job j is scheduled inside the busy interval.
  Section InterferenceIsComplement.

Consider any subinterval [t, t + delta) inside the busy interval [t1, t2).
    Variables (t : instant) (delta : duration).
    Hypothesis H_greater_than_or_equal : t1 ≤ t.
    Hypothesis H_less_or_equal: t + delta ≤ t2.

We prove that sum of cumulative service and cumulative interference in the interval [t, t + delta) is equal to delta.
    Lemma interference_is_complement_to_schedule:
      service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 203)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  ============================
  service_during sched j t (t + delta) + cumul_interference j t (t + delta) =
  delta

----------------------------------------------------------------------------- *)

    Proof.
      rewrite /service_during /cumul_interference/service_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 218)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  ============================
  \sum_(t <= t0 < t + delta) service_in j (sched t0) +
  definitions.cumul_interference interference j t (t + delta) = delta

----------------------------------------------------------------------------- *)

      rewrite -big_split //=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 229)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  ============================
  \sum_(t <= i < t + delta) (service_in j (sched i) + interference j i) =
  delta

----------------------------------------------------------------------------- *)

      rewrite -{2}(sum_of_ones t delta).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 253)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  ============================
  \sum_(t <= i < t + delta) (service_in j (sched i) + interference j i) =
  \sum_(t <= x < t + delta) 1

----------------------------------------------------------------------------- *)

      rewrite big_nat [in RHS]big_nat.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 277)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  ============================
  \sum_(t <= i < t + delta | t <= i < t + delta)
     (service_in j (sched i) + interference j i) =
  \sum_(t <= i < t + delta | t <= i < t + delta) 1

----------------------------------------------------------------------------- *)

      apply: eq_bigr⇒ x /andP[Lo Hi].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 370)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  x : nat
  Lo : t <= x
  Hi : x < t + delta
  ============================
  service_in j (sched x) + interference j x = 1

----------------------------------------------------------------------------- *)

      move: (H_work_conserving j t1 t2 x) ⇒ Workj.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 372)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  x : nat
  Lo : t <= x
  Hi : x < t + delta
  Workj : arrives_in arr_seq j ->
          job_task j = tsk ->
          0 < job_cost j ->
          definitions.busy_interval sched interference interfering_workload j
            t1 t2 ->
          t1 <= x < t2 -> ~ interference j x <-> scheduled_at sched j x
  ============================
  service_in j (sched x) + interference j x = 1

----------------------------------------------------------------------------- *)

      feed_n 5 Workj; try done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 397)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  x : nat
  Lo : t <= x
  Hi : x < t + delta
  Workj : t1 <= x < t2 -> ~ interference j x <-> scheduled_at sched j x
  ============================
  t1 <= x < t2

subgoal 2 (ID 402) is:
 service_in j (sched x) + interference j x = 1

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 397)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  x : nat
  Lo : t <= x
  Hi : x < t + delta
  Workj : t1 <= x < t2 -> ~ interference j x <-> scheduled_at sched j x
  ============================
  t1 <= x < t2

----------------------------------------------------------------------------- *)

by apply/andP; split; eapply leq_trans; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 402)

subgoal 1 (ID 402) is:
 service_in j (sched x) + interference j x = 1

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 402)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  x : nat
  Lo : t <= x
  Hi : x < t + delta
  Workj : ~ interference j x <-> scheduled_at sched j x
  ============================
  service_in j (sched x) + interference j x = 1

----------------------------------------------------------------------------- *)

      rewrite -/(service_at sched j x) service_at_is_scheduled_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 505)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  x : nat
  Lo : t <= x
  Hi : x < t + delta
  Workj : ~ interference j x <-> scheduled_at sched j x
  ============================
  scheduled_at sched j x + interference j x = 1

----------------------------------------------------------------------------- *)

      have->: scheduled_at sched j x = ~~ interference j x.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 511)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  x : nat
  Lo : t <= x
  Hi : x < t + delta
  Workj : ~ interference j x <-> scheduled_at sched j x
  ============================
  scheduled_at sched j x = ~~ interference j x

subgoal 2 (ID 516) is:
 ~~ interference j x + interference j x = 1

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 511)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  x : nat
  Lo : t <= x
  Hi : x < t + delta
  Workj : ~ interference j x <-> scheduled_at sched j x
  ============================
  scheduled_at sched j x = ~~ interference j x

----------------------------------------------------------------------------- *)

by apply/idP/negP; intuition.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 516)

subgoal 1 (ID 516) is:
 ~~ interference j x + interference j x = 1

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 516)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  delta : duration
  H_greater_than_or_equal : t1 <= t
  H_less_or_equal : t + delta <= t2
  x : nat
  Lo : t <= x
  Hi : x < t + delta
  Workj : ~ interference j x <-> scheduled_at sched j x
  ============================
  ~~ interference j x + interference j x = 1

----------------------------------------------------------------------------- *)

      exact: addn_negb.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

  End InterferenceIsComplement.

In this section, we prove a sufficient condition under which job j receives enough service.
  Section InterferenceBoundedImpliesEnoughService.

Let progress_of_job be the desired service of job j.
    Variable progress_of_job : duration.
    Hypothesis H_progress_le_job_cost : progress_of_job ≤ job_cost j.

Assume that for some delta, the sum of desired progress and cumulative interference is bounded by delta (i.e., the supply).
    Variable delta : duration.
    Hypothesis H_total_workload_is_bounded:
      progress_of_job + cumul_interference j t1 (t1 + delta) ≤ delta.

Then, it must be the case that the job has received no less service than progress_of_job.
    Theorem j_receives_at_least_run_to_completion_threshold:
      service sched j (t1 + delta) ≥ progress_of_job.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 203)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  ============================
  progress_of_job <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

    Proof.
      case NEQ: (t1 + delta ≤ t2); last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 275)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = false
  ============================
  progress_of_job <= service sched j (t1 + delta)

subgoal 2 (ID 243) is:
 progress_of_job <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 275)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = false
  ============================
  progress_of_job <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

intros.
        have L8 := job_completes_within_busy_interval.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 280)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = false
  L8 : completed_by sched j t2
  ============================
  progress_of_job <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

        apply leq_trans with (job_cost j); first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 284)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = false
  L8 : completed_by sched j t2
  ============================
  job_cost j <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

        rewrite /service.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 291)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = false
  L8 : completed_by sched j t2
  ============================
  job_cost j <= service_during sched j 0 (t1 + delta)

----------------------------------------------------------------------------- *)

        rewrite -(service_during_cat _ _ _ t2).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 313)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = false
  L8 : completed_by sched j t2
  ============================
  job_cost j <=
  service_during sched j 0 t2 + service_during sched j t2 (t1 + delta)

subgoal 2 (ID 314) is:
 0 <= t2 <= t1 + delta

----------------------------------------------------------------------------- *)

        apply leq_trans with (service_during sched j 0 t2); [by done | by rewrite leq_addr].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 314)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = false
  L8 : completed_by sched j t2
  ============================
  0 <= t2 <= t1 + delta

----------------------------------------------------------------------------- *)

          by apply/andP; split; last (apply negbT in NEQ; apply ltnW; rewrite ltnNge).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 243)

subgoal 1 (ID 243) is:
 progress_of_job <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 243)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  ============================
  progress_of_job <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 243)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  ============================
  progress_of_job <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

 move: H_total_workload_is_bounded ⇒ BOUND.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 359)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job + cumul_interference j t1 (t1 + delta) <= delta
  ============================
  progress_of_job <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

         apply subh3 in BOUND.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 360)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job <= delta - cumul_interference j t1 (t1 + delta)
  ============================
  progress_of_job <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

         apply leq_trans with (delta - cumul_interference j t1 (t1 + delta)); first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 363)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job <= delta - cumul_interference j t1 (t1 + delta)
  ============================
  delta - cumul_interference j t1 (t1 + delta) <=
  service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

         apply leq_trans with (service_during sched j t1 (t1 + delta)).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 367)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job <= delta - cumul_interference j t1 (t1 + delta)
  ============================
  delta - cumul_interference j t1 (t1 + delta) <=
  service_during sched j t1 (t1 + delta)

subgoal 2 (ID 368) is:
 service_during sched j t1 (t1 + delta) <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

         {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 367)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job <= delta - cumul_interference j t1 (t1 + delta)
  ============================
  delta - cumul_interference j t1 (t1 + delta) <=
  service_during sched j t1 (t1 + delta)

----------------------------------------------------------------------------- *)

rewrite -{1}[delta](interference_is_complement_to_schedule t1) //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 373)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job <= delta - cumul_interference j t1 (t1 + delta)
  ============================
  service_during sched j t1 (t1 + delta) +
  cumul_interference j t1 (t1 + delta) - cumul_interference j t1 (t1 + delta) <=
  service_during sched j t1 (t1 + delta)

----------------------------------------------------------------------------- *)

           rewrite -addnBA // subnn addn0 //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 368)

subgoal 1 (ID 368) is:
 service_during sched j t1 (t1 + delta) <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

         }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 368)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job <= delta - cumul_interference j t1 (t1 + delta)
  ============================
  service_during sched j t1 (t1 + delta) <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

         {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 368)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job <= delta - cumul_interference j t1 (t1 + delta)
  ============================
  service_during sched j t1 (t1 + delta) <= service sched j (t1 + delta)

----------------------------------------------------------------------------- *)

rewrite /service -[X in _ ≤ X](service_during_cat _ _ _ t1).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 470)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job <= delta - cumul_interference j t1 (t1 + delta)
  ============================
  service_during sched j t1 (t1 + delta) <=
  service_during sched j 0 t1 + service_during sched j t1 (t1 + delta)

subgoal 2 (ID 471) is:
 0 <= t1 <= t1 + delta

----------------------------------------------------------------------------- *)

           rewrite leq_addl //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 471)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  progress_of_job : duration
  H_progress_le_job_cost : progress_of_job <= job_cost j
  delta : duration
  H_total_workload_is_bounded : progress_of_job +
                                cumul_interference j t1 (t1 + delta) <= delta
  NEQ : (t1 + delta <= t2) = true
  BOUND : progress_of_job <= delta - cumul_interference j t1 (t1 + delta)
  ============================
  0 <= t1 <= t1 + delta

----------------------------------------------------------------------------- *)

             by apply/andP; split; last rewrite leq_addr.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

         }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

  End InterferenceBoundedImpliesEnoughService.

In this section we prove a simple lemma about completion of a job after is reaches run-to-completion threshold.
  Section CompletionOfJobAfterRunToCompletionThreshold.

Assume that completed jobs do not execute ...
    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute sched.

.. and the preemption model is valid.
    Hypothesis H_valid_preemption_model:
      valid_preemption_model arr_seq sched.

Then, job j must complete in [job_cost j - job_run_to_completion_threshold j] time units after it reaches run-to-completion threshold.
    Lemma job_completes_after_reaching_run_to_completion_threshold:
      ∀ t,
        job_run_to_completion_threshold j ≤ service sched j t →
        completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 223)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  ============================
  forall t : instant,
  job_run_to_completion_threshold j <= service sched j t ->
  completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j))

----------------------------------------------------------------------------- *)

    Proof.
      move ⇒ t ES.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 225)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  ============================
  completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j))

----------------------------------------------------------------------------- *)

      set (job_cost j - job_run_to_completion_threshold j) as job_last.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 232)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  ============================
  completed_by sched j (t + job_last)

----------------------------------------------------------------------------- *)

      have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
                     Job H2 H3 _ _ arr_seq sched _ j _ t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 245)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  ============================
  completed_by sched j (t + job_last)

----------------------------------------------------------------------------- *)

      apply negbNE; apply/negP; intros CONTR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 268)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  ============================
  False

----------------------------------------------------------------------------- *)

      have SCHED: ∀ t', t ≤ t' ≤ t + job_last → scheduled_at sched j t'.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 273)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  ============================
  forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'

subgoal 2 (ID 275) is:
 False

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 273)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  ============================
  forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'

----------------------------------------------------------------------------- *)

move ⇒ t' /andP [GE LT].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 316)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  t' : nat
  GE : t <= t'
  LT : t' <= t + job_last
  ============================
  scheduled_at sched j t'

----------------------------------------------------------------------------- *)

        rewrite -[t'](@subnKC t) //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 320)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  t' : nat
  GE : t <= t'
  LT : t' <= t + job_last
  ============================
  scheduled_at sched j (t + (t' - t))

----------------------------------------------------------------------------- *)

        eapply LSNP; eauto 2; first by rewrite leq_addr.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 348)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  t' : nat
  GE : t <= t'
  LT : t' <= t + job_last
  ============================
  ~~ completed_by sched j (t + (t' - t))

----------------------------------------------------------------------------- *)

        rewrite subnKC //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 378)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  t' : nat
  GE : t <= t'
  LT : t' <= t + job_last
  ============================
  ~~ completed_by sched j t'

----------------------------------------------------------------------------- *)

        apply/negP; intros COMPL.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 423)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  t' : nat
  GE : t <= t'
  LT : t' <= t + job_last
  COMPL : completed_by sched j t'
  ============================
  False

----------------------------------------------------------------------------- *)

        move: CONTR ⇒ /negP Temp; apply: Temp.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 457)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  t' : nat
  GE : t <= t'
  LT : t' <= t + job_last
  COMPL : completed_by sched j t'
  ============================
  completed_by sched j (t + job_last)

----------------------------------------------------------------------------- *)

        apply completion_monotonic with (t0 := t'); try done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 275)

subgoal 1 (ID 275) is:
 False

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 275)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  ============================
  False

----------------------------------------------------------------------------- *)

      have SERV: job_last + 1 ≤ \sum_(t ≤ t' < t + (job_last + 1)) service_at sched j t'.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 471)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  ============================
  job_last + 1 <= \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'

subgoal 2 (ID 473) is:
 False

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 471)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  ============================
  job_last + 1 <= \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'

----------------------------------------------------------------------------- *)

rewrite -{1}[job_last + 1]addn0 -{2}(subnn t) addnBA // addnC.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 515)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  ============================
  t + (job_last + 1) - t <=
  \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'

----------------------------------------------------------------------------- *)

        rewrite -{1}[_+_-_]addn0 -[_+_-_]mul1n -iter_addn -big_const_nat.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 550)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  ============================
  \sum_(t <= i < t + (job_last + 1)) 1 <=
  \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'

----------------------------------------------------------------------------- *)

        rewrite big_nat_cond [in X in _ ≤ X]big_nat_cond.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 573)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  ============================
  \sum_(t <= i < t + (job_last + 1) | (t <= i < t + (job_last + 1)) && true)
     1 <=
  \sum_(t <= i < t + (job_last + 1) | (t <= i < t + (job_last + 1)) && true)
     service_at sched j i

----------------------------------------------------------------------------- *)

        rewrite leq_sum //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 582)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  ============================
  forall i : nat,
  (t <= i < t + (job_last + 1)) && true -> 0 < service_at sched j i

----------------------------------------------------------------------------- *)

        move ⇒ t' /andP [NEQ _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 649)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  t' : nat
  NEQ : t <= t' < t + (job_last + 1)
  ============================
  0 < service_at sched j t'

----------------------------------------------------------------------------- *)

        rewrite service_at_is_scheduled_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 656)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  t' : nat
  NEQ : t <= t' < t + (job_last + 1)
  ============================
  0 < scheduled_at sched j t'

----------------------------------------------------------------------------- *)

          by rewrite lt0b; apply SCHED; rewrite addn1 addnS ltnS in NEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 473)

subgoal 1 (ID 473) is:
 False

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 473)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  SERV : job_last + 1 <=
         \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'
  ============================
  False

----------------------------------------------------------------------------- *)

      eapply service_at_most_cost with (j0 := j) (t0 := t + job_last.+1) in H_completed_jobs_dont_execute; last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 721)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  SERV : job_last + 1 <=
         \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'
  ============================
  unit_service_proc_model (processor_state Job)

subgoal 2 (ID 719) is:
 False

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 721)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  t : instant
  ES : job_run_to_completion_threshold j <= service sched j t
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  SERV : job_last + 1 <=
         \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'
  ============================
  unit_service_proc_model (processor_state Job)

----------------------------------------------------------------------------- *)

by apply ideal_proc_model_provides_unit_service.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 719)

subgoal 1 (ID 719) is:
 False

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 719)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
                                  job_cost j
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  ES : job_run_to_completion_threshold j <= service sched j t
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  SERV : job_last + 1 <=
         \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'
  ============================
  False

----------------------------------------------------------------------------- *)

      move: H_completed_jobs_dont_execute; rewrite leqNgt; move ⇒ /negP T; apply: T.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 759)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
                                  job_cost j
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  ES : job_run_to_completion_threshold j <= service sched j t
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  SERV : job_last + 1 <=
         \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'
  ============================
  job_cost j < service sched j (t + succn job_last)

----------------------------------------------------------------------------- *)

      rewrite /service -(service_during_cat _ _ _ t); last by (apply/andP; split; last rewrite leq_addr).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 788)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
                                  job_cost j
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  ES : job_run_to_completion_threshold j <= service sched j t
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  SERV : job_last + 1 <=
         \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'
  ============================
  job_cost j <
  service_during sched j 0 t + service_during sched j t (t + succn job_last)

----------------------------------------------------------------------------- *)

      apply leq_trans with (job_run_to_completion_threshold j + service_during sched j t (t + job_last.+1));
        last by rewrite leq_add2r.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 827)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
                                  job_cost j
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  ES : job_run_to_completion_threshold j <= service sched j t
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  SERV : job_last + 1 <=
         \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'
  ============================
  job_cost j <
  job_run_to_completion_threshold j +
  service_during sched j t (t + succn job_last)

----------------------------------------------------------------------------- *)

      apply leq_trans with (job_run_to_completion_threshold j + job_last.+1); last by rewrite leq_add2l /service_during -addn1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 837)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost
                                   arr_seq
  tsk : Task
  interference : Job -> instant -> bool
  interfering_workload : Job -> instant -> duration
  work_conserving := definitions.work_conserving arr_seq sched tsk
   : (Job -> instant -> bool) -> (Job -> instant -> duration) -> Prop
  cumul_interference := definitions.cumul_interference interference
   : Job -> nat -> nat -> nat
  cumul_interfering_workload := definitions.cumul_interfering_workload
                                  interfering_workload
   : Job -> nat -> nat -> nat
  busy_interval := definitions.busy_interval sched interference
                     interfering_workload : Job -> instant -> instant -> Prop
  H_work_conserving : work_conserving interference interfering_workload
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  H_job_cost_positive : job_cost_positive j
  t1, t2 : instant
  H_busy_interval : busy_interval j t1 t2
  t : instant
  job_last := job_cost j - job_run_to_completion_threshold j : nat
  H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
                                  job_cost j
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  ES : job_run_to_completion_threshold j <= service sched j t
  LSNP : forall p : ProcessorState Job (processor_state Job),
         valid_preemption_model arr_seq sched ->
         arrives_in arr_seq j ->
         forall t' : nat,
         t <= t' ->
         job_run_to_completion_threshold j <= service sched j t ->
         ~~ completed_by sched j t' -> scheduled_at sched j t'
  CONTR : ~~ completed_by sched j (t + job_last)
  SCHED : forall t' : nat, t <= t' <= t + job_last -> scheduled_at sched j t'
  SERV : job_last + 1 <=
         \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'
  ============================
  job_cost j < job_run_to_completion_threshold j + succn job_last

----------------------------------------------------------------------------- *)

        by rewrite addnS ltnS subnKC //; eapply job_run_to_completion_threshold_le_job_cost; eauto.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

  End CompletionOfJobAfterRunToCompletionThreshold.

End AbstractRTARunToCompletionThreshold.