Require Export prosa.analysis.facts.model.ideal.schedule.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.abstract.search_space.
Require Export prosa.analysis.abstract.abstract_rta.
Require Export prosa.analysis.abstract.iw_auxiliary.

(** * Abstract Response-Time Analysis For Processor State with Ideal Uni-Service Progress Model *)
(** In this module, we present an instantiation of the general
    response-time analysis framework for models that satisfy the ideal
    uni-service progress assumptions. *)

(** We prove that the maximum (with respect to the set of offsets)
    among the solutions of the response-time bound recurrence is a
    response-time bound for [tsk]. Note that in this section we add
    additional restrictions on the processor state. These assumptions
    allow us to eliminate the second equation from [aRTA+]'s
    recurrence since jobs experience no delays while executing
    non-preemptively. *)
Section AbstractRTAIdeal.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskRunToCompletionThreshold Task}.

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

  (** Consider any kind of uni-service ideal processor state model. *)
  Context `{PState : ProcessorState Job}.
  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, non-duplicate arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** Next, consider any schedule of this arrival sequence... *)
  Variable sched : schedule PState.
  Hypothesis H_jobs_come_from_arrival_sequence:
    jobs_come_from_arrival_sequence sched arr_seq.

  (** ... where jobs do not execute before their arrival nor after completion. *)
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

  (** Assume that the job costs are no larger than the task costs. *)
  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.

  (** Consider a task set [ts]... *)
  Variable ts : list Task.

  (** ... and a task [tsk] of [ts] that is to be analyzed. *)
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

  (** Consider a valid preemption model... *)
  Hypothesis H_valid_preemption_model :
    valid_preemption_model arr_seq sched.

  (** ...and a valid task run-to-completion threshold function. That
      is, [task_rtc tsk] is (1) no bigger than [tsk]'s cost and (2)
      for any job [j] of task [tsk] [job_rtct j] is bounded by
      [task_rtct tsk]. *)
  Hypothesis H_valid_run_to_completion_threshold :
    valid_task_run_to_completion_threshold arr_seq tsk.

  (** Assume we are provided with abstract functions for Interference
      and Interfering Workload. *)
  Context `{Interference Job}.
  Context `{InterferingWorkload Job}.

  (** We assume that the scheduler is work-conserving. *)
  Hypothesis H_work_conserving : work_conserving arr_seq sched.

  (** Let [L] be a constant that bounds any busy interval of task [tsk]. *)
  Variable L : duration.
  Hypothesis H_busy_interval_exists :
    busy_intervals_are_bounded_by arr_seq sched tsk L.

  (** Next, assume that [interference_bound_function] is a bound on
      the interference incurred by jobs of task [tsk] parametrized by
      the relative arrival time [A]. *)
  Variable interference_bound_function : (* A *) duration -> (* Δ *) duration -> duration.
  Hypothesis H_job_interference_is_bounded :
    job_interference_is_bounded_by
      arr_seq sched tsk interference_bound_function (relative_arrival_time_of_job_is_A sched).

  (** To apply the generalized aRTA, we have to instantiate [IBF_P]
      and [IBF_NP]. In this file, we assume we are given a generic function
      [interference_bound_function] that bounds interference of jobs
      of tasks in [ts] and which have to be instantiated in subsequent
      files. We use this function to instantiate [IBF_P]. *)

  (** However, we still have to instantiate function [IBF_NP], which
      is a function that bounds interference in a non-preemptive stage
      of execution. We prove that this function can be instantiated
      with a constant function [λ F Δ ⟹ F - task_rtct tsk]. *)
  Let IBF_NP (F : duration) (Δ : duration) := F - task_rtct tsk.

  (** Let us re-iterate on the intuitive interpretation of this
      function. Since [F] is a solution to the first equation
      [task_rtct tsk + IBF_P tsk A F <= F], we know that by time
      instant [t1 + F] a job receives [task_rtct tsk] units of service
      and, hence, it becomes non-preemptive. Given this information,
      how can we bound the job's interference in an interval <<[t1, t1
      + R)>>? Note that this interval starts with the beginning of the
      busy interval. We know that the job receives [F - task_rtct tsk]
      units of interference, and there will no more
      interference. Hence, [IBF_NP tsk F Δ := F - task_rtct tsk]. *)
  Lemma nonpreemptive_interference_is_bounded :
    job_interference_is_bounded_by
      arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk interference_bound_function).
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
job_interference_is_bounded_by arr_seq sched tsk
  IBF_NP
  (relative_time_to_reach_rtct sched tsk
     interference_bound_function)
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
job_interference_is_bounded_by arr_seq sched tsk
  IBF_NP
  (relative_time_to_reach_rtct sched tsk
     interference_bound_function)
    move => t1 t2 Δ j ARR TSK BUSY LT NCOM F RTC; specialize (RTC _ _ BUSY).
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
RTC: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) <=
IBF_NP F Δ
    have POS : 0 < job_cost j.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
RTC: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
0 < job_cost j
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
RTC: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
POS: 0 < job_cost j
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) <=
IBF_NP F Δ
    {
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
RTC: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
0 < job_cost j move_neq_up ZE; move: ZE; rewrite leqn0; move => /eqP ZE.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
RTC: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
ZE: job_cost j = 0
False
      move: NCOM => /negP NCOM; apply: NCOM.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
F: nat
RTC: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
ZE: job_cost j = 0
completed_by sched j (t1 + Δ)
      by rewrite /completed_by ZE.
    }
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
RTC: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
POS: 0 < job_cost j
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) <=
IBF_NP F Δ
    move: (BUSY) => [PREF _].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
RTC: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) <=
IBF_NP F Δ
    move : (TSK) (BUSY) RTC => /eqP TSKeq [[/andP [LE1 LE2] [QT1 AQT]] QT2] [LEQ RTC].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) <=
IBF_NP F Δ
    rewrite leq_subRL_impl // addnC -/cumulative_interference.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
    destruct (leqP t2 (t1 + F)) as [NEQ1|NEQ1]; last destruct (leqP F Δ) as [NEQ2|NEQ2].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t2 <= t1 + F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: Δ < F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
    {
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t2 <= t1 + F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F rewrite -leq_subLR in NEQ1.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t2 - t1 <= F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
      rewrite -(leqRW NEQ1) (leqRW RTC) (leqRW (service_at_most_cost _ _ _ _ _)) //
              (leqRW (service_within_busy_interval_ge_job_cost  _ _ _ _ _ _ _)) //.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t2 - t1 <= F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
service_during sched j t1 t2 <= t2 - t1
      rewrite (leqRW (cumulative_interference_sub _ _ t1 _ t1 t2 _ _)) //.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t2 - t1 <= F
cumul_cond_interference (fun=> xpredT) j t1 t2 +
service_during sched j t1 t2 <= t2 - t1 
      have LLL : (t1 < t2) = true by apply leq_ltn_trans with (t1 + Δ); lia.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t2 - t1 <= F
LLL: (t1 < t2) = true
cumul_cond_interference (fun=> xpredT) j t1 t2 +
service_during sched j t1 t2 <= t2 - t1
      interval_to_duration t1 t2 k.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
k: nat
LT: t1 + Δ < t1 + k
BUSY: definitions.busy_interval sched j t1 (t1 + k)
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1
  (t1 + k)
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t1 + k
QT1: definitions.quiet_time sched j t1
QT2: definitions.quiet_time sched j (t1 + k)
AQT: forall t : nat,
t1 < t < t1 + k ->
~ definitions.quiet_time sched j t
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + k - t1 <= F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + k) +
service_during sched j t1 (t1 + k) <= t1 + k - t1
      eapply leq_trans.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
k: nat
LT: t1 + Δ < t1 + k
BUSY: definitions.busy_interval sched j t1 (t1 + k)
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1
  (t1 + k)
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t1 + k
QT1: definitions.quiet_time sched j t1
QT2: definitions.quiet_time sched j (t1 + k)
AQT: forall t : nat,
t1 < t < t1 + k ->
~ definitions.quiet_time sched j t
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + k - t1 <= F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + k) +
service_during sched j t1 (t1 + k) <= ?n
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
k: nat
LT: t1 + Δ < t1 + k
BUSY: definitions.busy_interval sched j t1 (t1 + k)
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1
  (t1 + k)
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t1 + k
QT1: definitions.quiet_time sched j t1
QT2: definitions.quiet_time sched j (t1 + k)
AQT: forall t : nat,
t1 < t < t1 + k ->
~ definitions.quiet_time sched j t
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + k - t1 <= F
?n <= t1 + k - t1
      -
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
k: nat
LT: t1 + Δ < t1 + k
BUSY: definitions.busy_interval sched j t1 (t1 + k)
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1
  (t1 + k)
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t1 + k
QT1: definitions.quiet_time sched j t1
QT2: definitions.quiet_time sched j (t1 + k)
AQT: forall t : nat,
t1 < t < t1 + k ->
~ definitions.quiet_time sched j t
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + k - t1 <= F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + k) +
service_during sched j t1 (t1 + k) <= ?n by rewrite addnC; (eapply service_and_interference_bounded with (t := t1) (t3 := t1+k)
                        || eapply service_and_interference_bounded with (t := t1) (t2 := t1+k)).
      -
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
k: nat
LT: t1 + Δ < t1 + k
BUSY: definitions.busy_interval sched j t1 (t1 + k)
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1
  (t1 + k)
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t1 + k
QT1: definitions.quiet_time sched j t1
QT2: definitions.quiet_time sched j (t1 + k)
AQT: forall t : nat,
t1 < t < t1 + k ->
~ definitions.quiet_time sched j t
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + k - t1 <= F
k <= t1 + k - t1 lia.
    }
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: Δ < F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
    {
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F have NoInterference: cumulative_interference j (t1 + F) (t1 + Δ) = 0.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
cumulative_interference j (t1 + F) (t1 + Δ) = 0
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
NoInterference: cumulative_interference j 
  (t1 + F) 
  (t1 + Δ) = 0
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
      {
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
cumulative_interference j (t1 + F) (t1 + Δ) = 0 rewrite /cumulative_interference /cumul_cond_interference big_nat.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
\sum_(t1 + F <= i < t1 + Δ | t1 + F <= i < t1 + Δ)
   cond_interference (fun=> xpredT) j i = 0
        apply big1; move => t /andP [GE__t LT__t].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
GE__t: t1 + F <= t
LT__t: t < t1 + Δ
cond_interference (fun=> xpredT) j t = 0
        apply/eqP; rewrite eqb0; apply/negP; eapply H_work_conserving => //.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
GE__t: t1 + F <= t
LT__t: t < t1 + Δ
t1 <= t < t2
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
GE__t: t1 + F <= t
LT__t: t < t1 + Δ
receives_service_at sched j t
        {
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
GE__t: t1 + F <= t
LT__t: t < t1 + Δ
t1 <= t < t2 by apply/andP; split; lia. }
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
GE__t: t1 + F <= t
LT__t: t < t1 + Δ
receives_service_at sched j t
        apply: H_ideal_progress_proc_model.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
GE__t: t1 + F <= t
LT__t: t < t1 + Δ
scheduled_in j (sched t)
        apply: job_nonpreemptive_after_run_to_completion_threshold GE__t _ _ => //.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
LT__t: t < t1 + Δ
job_rtct j <= service sched j (t1 + F)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
LT__t: t < t1 + Δ
~~ completed_by sched j t
        -
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
LT__t: t < t1 + Δ
job_rtct j <= service sched j (t1 + F) by rewrite -(leqRW RTC); apply H_valid_run_to_completion_threshold.
        -
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
t: nat
LT__t: t < t1 + Δ
~~ completed_by sched j t by move: NCOM; apply contra; apply completion_monotonic; lia.
      }
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
NoInterference: cumulative_interference j 
  (t1 + F) 
  (t1 + Δ) = 0
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
      rewrite (leqRW RTC); erewrite cumulative_interference_cat with (t := t1 + F); last by lia.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
NoInterference: cumulative_interference j 
  (t1 + F) 
  (t1 + Δ) = 0
cumul_cond_interference (fun=> xpredT) j t1 (t1 + F) +
cumul_cond_interference (fun=> xpredT) j (t1 + F)
  (t1 + Δ) + service sched j (t1 + F) <= F
      rewrite /cumulative_interference in NoInterference.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
NoInterference: cumul_cond_interference
  (fun=> xpredT) j 
  (t1 + F) 
  (t1 + Δ) = 0
cumul_cond_interference (fun=> xpredT) j t1 (t1 + F) +
cumul_cond_interference (fun=> xpredT) j (t1 + F)
  (t1 + Δ) + service sched j (t1 + F) <= F
      rewrite NoInterference addn0; erewrite no_service_before_busy_interval => //.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: F <= Δ
NoInterference: cumul_cond_interference
  (fun=> xpredT) j 
  (t1 + F) 
  (t1 + Δ) = 0
cumul_cond_interference (fun=> xpredT) j t1 (t1 + F) +
service_during sched j t1 (t1 + F) <= F
      by rewrite addnC; apply: service_and_interference_bounded.
    }
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: Δ < F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
    {
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: Δ < F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F rewrite (leqRW RTC) (leqRW (cumulative_interference_sub _ _ t1 _ t1 (t1 + F) _ _ )); try lia.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: Δ < F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + F) +
service sched j (t1 + F) <= F
      erewrite no_service_before_busy_interval => //.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
t1, t2: instant
Δ: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + Δ < t2
NCOM: ~~ completed_by sched j (t1 + Δ)
F: nat
POS: 0 < job_cost j
PREF: definitions.busy_interval_prefix sched j t1 t2
TSKeq: job_task j = tsk
LE1: t1 <= job_arrival j
LE2: job_arrival j < t2
QT1: definitions.quiet_time sched j t1
AQT: forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j t
QT2: definitions.quiet_time sched j t2
LEQ: task_rtct tsk +
interference_bound_function 
  (job_arrival j - t1) F <= F
RTC: task_rtct tsk <= service sched j (t1 + F)
NEQ1: t1 + F < t2
NEQ2: Δ < F
cumul_cond_interference (fun=> xpredT) j t1 (t1 + F) +
service_during sched j t1 (t1 + F) <= F
      by rewrite addnC; eapply service_and_interference_bounded. }
  Qed.

  (** For simplicity, let's define a local name for the search space. *)
  Let is_in_search_space A := is_in_search_space L interference_bound_function A.

  (** Consider any value [R] that upper-bounds the solution of each
      response-time recurrence, i.e., for any relative arrival time A
      in the search space, there exists a corresponding solution [F]
      such that [F + (task_cost tsk - task_rtc tsk) <= R]. *)
  Variable R : duration.
  Hypothesis H_R_is_maximum_ideal :
    forall A,
      is_in_search_space A ->
      exists F,
        task_rtct tsk + interference_bound_function A (A + F) <= A + F /\
        F + (task_cost tsk - task_rtct tsk) <= R.

  (** Using the lemma about [IBF_NP], we instantiate the general RTA
      theorem's result to the ideal uniprocessor's case to prove that
      [R] is a response-time bound. *)
  Theorem uniprocessor_response_time_bound_ideal :
    task_response_time_bound arr_seq sched tsk R.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
task_response_time_bound arr_seq sched tsk R
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
task_response_time_bound arr_seq sched tsk R
    eapply uniprocessor_response_time_bound with (IBF_NP := fun F Δ => F - task_rtct tsk) => //.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
job_interference_is_bounded_by arr_seq sched tsk
  (fun F : nat => fun=> F - task_rtct tsk)
  (relative_time_to_reach_rtct sched tsk
     interference_bound_function)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
forall F : nat,
duration -> F <= task_cost tsk + (F - task_rtct tsk)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
forall A : duration,
search_space.is_in_search_space L
  interference_bound_function A ->
exists F : duration,
  task_rtct tsk + interference_bound_function A F <= F /\
  task_cost tsk + (F - task_rtct tsk) <= A + R
    {
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
job_interference_is_bounded_by arr_seq sched tsk
  (fun F : nat => fun=> F - task_rtct tsk)
  (relative_time_to_reach_rtct sched tsk
     interference_bound_function) by apply nonpreemptive_interference_is_bounded. }
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
forall F : nat,
duration -> F <= task_cost tsk + (F - task_rtct tsk)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
forall A : duration,
search_space.is_in_search_space L
  interference_bound_function A ->
exists F : duration,
  task_rtct tsk + interference_bound_function A F <= F /\
  task_cost tsk + (F - task_rtct tsk) <= A + R
    {
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
forall F : nat,
duration -> F <= task_cost tsk + (F - task_rtct tsk) move => F _.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
F: nat
F <= task_cost tsk + (F - task_rtct tsk)
      destruct (leqP F (task_rtct tsk)) as [NEQ|NEQ].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
F: nat
NEQ: F <= task_rtct tsk
F <= task_cost tsk + (F - task_rtct tsk)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
F: nat
NEQ: task_rtct tsk < F
F <= task_cost tsk + (F - task_rtct tsk)
      -
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
F: nat
NEQ: F <= task_rtct tsk
F <= task_cost tsk + (F - task_rtct tsk) eapply leq_trans; [apply NEQ | ].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
F: nat
NEQ: F <= task_rtct tsk
task_rtct tsk <= task_cost tsk + (F - task_rtct tsk)
        by eapply leq_trans; [apply H_valid_run_to_completion_threshold | lia].
      -
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
F: nat
NEQ: task_rtct tsk < F
F <= task_cost tsk + (F - task_rtct tsk) by rewrite addnBCA; [lia | apply H_valid_run_to_completion_threshold | lia].
    }
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
forall A : duration,
search_space.is_in_search_space L
  interference_bound_function A ->
exists F : duration,
  task_rtct tsk + interference_bound_function A F <= F /\
  task_cost tsk + (F - task_rtct tsk) <= A + R
    {
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R: duration
H_R_is_maximum_ideal: forall A : nat,
is_in_search_space A ->
exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
forall A : duration,
search_space.is_in_search_space L
  interference_bound_function A ->
exists F : duration,
  task_rtct tsk + interference_bound_function A F <= F /\
  task_cost tsk + (F - task_rtct tsk) <= A + R move => A SP; specialize (H_R_is_maximum_ideal A SP).
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R, A: duration
H_R_is_maximum_ideal: exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
SP: search_space.is_in_search_space L
  interference_bound_function A
exists F : duration,
  task_rtct tsk + interference_bound_function A F <= F /\
  task_cost tsk + (F - task_rtct tsk) <= A + R
      destruct H_R_is_maximum_ideal as [F [EQ1 EQ2]].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R, A: duration
H_R_is_maximum_ideal: exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
SP: search_space.is_in_search_space L
  interference_bound_function A
F: nat
EQ1: task_rtct tsk +
interference_bound_function A (A + F) <= 
A + F
EQ2: F + (task_cost tsk - task_rtct tsk) <= R
exists F : duration,
  task_rtct tsk + interference_bound_function A F <= F /\
  task_cost tsk + (F - task_rtct tsk) <= A + R
      exists (A + F); split=> [//|].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R, A: duration
H_R_is_maximum_ideal: exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
SP: search_space.is_in_search_space L
  interference_bound_function A
F: nat
EQ1: task_rtct tsk +
interference_bound_function A (A + F) <= 
A + F
EQ2: F + (task_cost tsk - task_rtct tsk) <= R
task_cost tsk + (A + F - task_rtct tsk) <= A + R
      eapply leq_trans; [ | by erewrite leq_add2l; apply EQ2].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
PState: ProcessorState Job
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_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
H5: Interference Job
H6: InterferingWorkload Job
H_work_conserving: work_conserving arr_seq sched
L: duration
H_busy_interval_exists: busy_intervals_are_bounded_by
  arr_seq sched tsk L
interference_bound_function: duration ->
duration -> duration
H_job_interference_is_bounded: job_interference_is_bounded_by
  arr_seq sched tsk
  interference_bound_function
  (relative_arrival_time_of_job_is_A
     sched)
IBF_NP:= fun F : duration => fun=> F - task_rtct tsk: duration -> duration -> nat
is_in_search_space:= [eta search_space.is_in_search_space
       L
       interference_bound_function]: nat -> Prop
R, A: duration
H_R_is_maximum_ideal: exists F : nat,
  task_rtct tsk +
  interference_bound_function A
    (A + F) <= 
  A + F /\
  F +
  (task_cost tsk -
   task_rtct tsk) <= R
SP: search_space.is_in_search_space L
  interference_bound_function A
F: nat
EQ1: task_rtct tsk +
interference_bound_function A (A + F) <= 
A + F
EQ2: F + (task_cost tsk - task_rtct tsk) <= R
task_cost tsk + (A + F - task_rtct tsk) <=
A + (F + (task_cost tsk - task_rtct tsk))
      by rewrite addnBCA; [lia | apply H_valid_run_to_completion_threshold | lia].
    }
  Qed.

End AbstractRTAIdeal.