Library prosa.analysis.abstract.run_to_completion


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

Welcome to Coq 8.11.2 (June 2020)

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


Require Export prosa.analysis.facts.model.service_of_jobs.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export prosa.analysis.abstract.definitions.

Run-to-Completion Threshold of a job

In this module, we provide a sufficient condition under which a job receives enough service to become non-preemptive. 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 non-preemptive.
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 mapping jobs to their preemption points.
  Context `{JobPreemptable Job}.

Consider any kind of uni-service ideal processor state model.
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.
  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.

Consider any arrival sequence with consistent arrivals ...
... and any schedule of this arrival sequence.
  Variable sched : schedule PState.

Assume that the job costs are no larger than the task costs.
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.
For simplicity, let's define some local names.
We assume that the schedule is work-conserving.
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 665)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 746)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 747)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 803)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 804) is:
 completed_by sched j t2

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


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

1 subgoal (ID 803)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 804)

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

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


}

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

1 subgoal (ID 804)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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.
Consider any sub-interval [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 671)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 686)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 697)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 721)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 745)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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_bigrx /andP[Lo Hi].

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

1 subgoal (ID 838)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 840)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 865)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 870) is:
 service_in j (sched x) + interference j x = 1

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


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

1 subgoal (ID 865)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 870)

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

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


}

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

1 subgoal (ID 870)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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

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


      destruct interference.

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

2 subgoals (ID 973)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 : ~ true <-> scheduled_at sched j x
  ============================
  service_in j (sched x) + true = 1

subgoal 2 (ID 974) is:
 service_in j (sched x) + false = 1

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


      - replace (service_in _ _) with 0; auto; symmetry.

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

2 subgoals (ID 988)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 : ~ true <-> scheduled_at sched j x
  ============================
  service_in j (sched x) = 0

subgoal 2 (ID 974) is:
 service_in j (sched x) + false = 1

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


        apply no_service_not_scheduled; auto.

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

2 subgoals (ID 999)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 : ~ true <-> scheduled_at sched j x
  ============================
  ~~ scheduled_at sched j x

subgoal 2 (ID 974) is:
 service_in j (sched x) + false = 1

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


        now apply/negP; intros SCHED; apply Workj in SCHED; apply SCHED.

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

1 subgoal (ID 974)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 : ~ false <-> scheduled_at sched j x
  ============================
  service_in j (sched x) + false = 1

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


      - replace (service_in _ _) with 1; auto; symmetry.

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

1 subgoal (ID 1050)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 : ~ false <-> scheduled_at sched j x
  ============================
  service_in j (sched x) = 1

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


        apply/eqP; rewrite eqn_leq; apply/andP; split.

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

2 subgoals (ID 1135)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 : ~ false <-> scheduled_at sched j x
  ============================
  service_in j (sched x) <= 1

subgoal 2 (ID 1136) is:
 0 < service_in j (sched x)

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


        + apply H_unit_service_proc_model.

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

1 subgoal (ID 1136)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 : ~ false <-> scheduled_at sched j x
  ============================
  0 < service_in j (sched x)

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


        + now apply H_ideal_progress_proc_model, Workj.

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

No more subgoals.

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


    Qed.

  End InterferenceIsComplement.

In this section, we prove a sufficient condition under which job [j] receives enough service.
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 671)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 751)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 715) is:
 progress_of_job <= service sched j (t1 + delta)

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


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

1 subgoal (ID 751)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 756)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 760)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 767)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 789)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 790) 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 790)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 715)

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

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


      }

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

1 subgoal (ID 715)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 715)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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_boundedBOUND.

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

1 subgoal (ID 835)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 836)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 839)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 843)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 844) is:
 service_during sched j t1 (t1 + delta) <= service sched j (t1 + delta)

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


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

1 subgoal (ID 843)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 849)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 844)

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

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


         }

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

1 subgoal (ID 844)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 844)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 946)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 947) is:
 0 <= t1 <= t1 + delta

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


           rewrite leq_addl //.

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

1 subgoal (ID 947)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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.
Assume that completed jobs do not execute ...
.. and the preemption model is valid.
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 691)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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.
      movet ES.

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

1 subgoal (ID 693)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 700)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 713)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 736)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 741)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 743) is:
 False

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


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

1 subgoal (ID 741)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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'

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


movet' /andP [GE LT].

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

1 subgoal (ID 784)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 788)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 816)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 846)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 891)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 925)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 743)

subgoal 1 (ID 743) is:
 False

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


      }

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

1 subgoal (ID 743)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 939)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 941) is:
 False

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


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

1 subgoal (ID 939)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 983)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 1018)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 1041)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 1050)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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

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


        movet' /andP [NEQ _].

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

1 subgoal (ID 1117)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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'

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


        apply H_ideal_progress_proc_model; apply SCHED.

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

1 subgoal (ID 1119)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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)
  ============================
  t <= t' <= t + job_last

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


          by rewrite addn1 addnS ltnS in NEQ.

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

1 subgoal (ID 941)

subgoal 1 (ID 941) is:
 False

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


      }

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

1 subgoal (ID 941)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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; auto.

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

1 subgoal (ID 1182)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 1229)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 1258)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 1297)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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 1307)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptable Job
  PState : Type
  H4 : ProcessorState Job PState
  H_ideal_progress_proc_model : ideal_progress_proc_model PState
  H_unit_service_proc_model : unit_service_proc_model PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs 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 PState,
         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.