Require Export prosa.analysis.facts.priority.edf.
[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]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_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 Import prosa.model.readiness.basic.
Require Import prosa.model.priority.edf.
Require Import prosa.model.task.absolute_deadline.
Require Import prosa.analysis.abstract.ideal.cumulative_bounds.
Require Import prosa.analysis.facts.busy_interval.carry_in.
Require Import prosa.analysis.facts.readiness.basic.
Require Export prosa.analysis.abstract.ideal.abstract_seq_rta.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.facts.workload.edf_athep_bound.

(** * Abstract RTA for EDF-schedulers with Bounded Priority Inversion *)
(** In this module we instantiate the Abstract Response-Time analysis
    (aRTA) to EDF-schedulers for ideal uni-processor model of
    real-time tasks with arbitrary arrival models. *)

(** Given EDF priority policy and an ideal uni-processor scheduler
    model, we can explicitly specify [interference],
    [interfering_workload], and [interference_bound_function]. In this
    settings, we can define natural notions of service, workload, busy
    interval, etc. The important feature of this instantiation is that
    we can induce the meaningful notion of priority
    inversion. However, we do not specify the exact cause of priority
    inversion (as there may be different reasons for this, like
    execution of a non-preemptive segment or blocking due to resource
    locking). We only assume that that a priority inversion is
    bounded. *)

Section AbstractRTAforEDFwithArrivalCurves.

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

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

  (** We assume the classic (i.e., Liu & Layland) model of readiness
      without jitter or self-suspensions, wherein pending jobs are
      always ready. *)
  #[local] Existing Instance basic_ready_instance.

  (** For clarity, let's denote the relative deadline of a task as D. *)
  Let D tsk := task_deadline tsk.

  (** Consider the EDF policy that indicates a higher-or-equal
      priority relation. Note that we do not relate the EDF policy
      with the scheduler. However, we define functions for
      Interference and Interfering Workload that actively use the
      concept of priorities. *)
  Let EDF := EDF Job.

  (** 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 valid ideal uni-processor schedule of this arrival sequence
      that follows the scheduling policy. *)
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched EDF.

  (** To use the theorem [uniprocessor_response_time_bound_seq] from
      the Abstract RTA module, we need to specify functions of
      interference, interfering workload, and [task_IBF]. Next, we
      define interference and interfering workload; we return to
      [task_IBF] later. *)

  (** ** Instantiation of Interference *)
  (** We say that job [j] incurs interference at time [t] iff it
      cannot execute due to a higher-or-equal-priority job being
      scheduled, or if it incurs a priority inversion. *)
  #[local] Instance ideal_jlfp_interference : Interference Job :=
    ideal_jlfp_interference arr_seq sched.

  (** ** Instantiation of Interfering Workload *)
  (** The interfering workload, in turn, is defined as the sum of the
      priority inversion function and interfering workload of jobs
      with higher or equal priority. *)
  #[local] Instance ideal_jlfp_interfering_workload : InterferingWorkload Job :=
    ideal_jlfp_interfering_workload arr_seq sched.

  (** Note that we differentiate between abstract and classical
      notions of work-conserving schedule. *)
  Let work_conserving_ab := definitions.work_conserving arr_seq sched.
  Let work_conserving_cl := work_conserving.work_conserving arr_seq sched.

  (** We assume that the schedule is a work-conserving schedule
     in the _classical_ sense, and later prove that the hypothesis
     about abstract work-conservation also holds. *)
  Hypothesis H_work_conserving : work_conserving_cl.

  (** Assume that a job cost cannot be larger than a task cost. *)
  Hypothesis H_valid_job_cost :
    arrivals_have_valid_job_costs arr_seq.

  (** Consider an arbitrary task set ts. *)
  Variable ts : list Task.

  (** Next, we assume that all jobs come from the task set. *)
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

  (** Let max_arrivals be a family of valid arrival curves, i.e., for
      any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival bound
      of [tsk], and (2) it is a monotonic function that equals 0 for
      the empty interval delta = 0. *)
  Context `{MaxArrivals Task}.
  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

  (** Let [tsk] be any task in 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_rtct tsk] is (1) no bigger than [tsk]'s cost, (2) for
      any job of task [tsk] [job_rtct] is bounded by [task_rtct]. *)
  Hypothesis H_valid_run_to_completion_threshold:
    valid_task_run_to_completion_threshold arr_seq tsk.

  (** We introduce [rbf] as an abbreviation of the task request bound
      function, which is defined as [task_cost(T) × max_arrivals(T,Δ)]
      for some task [T]. *)
  Let rbf := task_request_bound_function.

  (** Next, we introduce [task_rbf] as an abbreviation of the task
      request bound function of task [tsk]. *)
  Let task_rbf := rbf tsk.

  (** Using the sum of individual request bound functions, we define
      the request bound function of all tasks (total request bound
      function). *)
  Let total_rbf := total_request_bound_function ts.

  (** Assume that there exists a bound on the length of any priority
      inversion experienced by any job of task [tsk]. Since we analyze
      only task [tsk], we ignore the lengths of priority inversions
      incurred by any other tasks. *)
  Variable priority_inversion_bound : duration -> duration.
  Hypothesis H_priority_inversion_is_bounded :
    priority_inversion_is_bounded_by
     arr_seq sched tsk priority_inversion_bound.

  (** Let [L] be any positive fixed point of the busy interval
      recurrence. *)
  Variable L : duration.
  Hypothesis H_L_positive : L > 0.
  Hypothesis H_fixed_point : L = total_rbf L.

  (** To reduce the time complexity of the analysis, we introduce the
      notion of search space for EDF. Intuitively, this corresponds to
      all "interesting" arrival offsets that the job under analysis
      might have with regard to the beginning of its busy-window. *)

  (** In the case of the search space for EDF, we consider three
      conditions. First, we ask whether [task_rbf A ≠ task_rbf (A +
      ε)]. *)
  Definition task_rbf_changes_at (A : duration) := task_rbf A != task_rbf (A + ε).

  (** Second, we ask whether there exists a task [tsko] from [ts] such
      that [tsko ≠ tsk] and [rbf(tsko, A + D tsk - D tsko) ≠ rbf(tsko,
      A + ε + D tsk - D tsko)]. Note that we use a slightly uncommon
      notation [has (λ tsko ⇒ P tskₒ) ts], which can be interpreted as
      follows: the task set [ts] contains a task [tsko] such that a
      predicate [P] holds for [tsko]. *)
  Definition bound_on_total_hep_workload_changes_at A :=
    has (fun tsko =>
           (tsk != tsko)
             && (rbf tsko (A + D tsk - D tsko)
                     != rbf tsko ((A + ε) + D tsk - D tsko))) ts.

  (** Third, we ask whether [priority_inversion_bound (A - ε) ≠
      priority_inversion_bound A]. *)
  Definition priority_inversion_changes_at (A : duration) :=
    priority_inversion_bound (A - ε) != priority_inversion_bound A.

  (** The final search space for EDF is a set of offsets that are less
      than [L] and where [priority_inversion_bound], [task_rbf], or
      [bound_on_total_hep_workload] changes in value. *)
  Definition is_in_search_space (A : duration) :=
    (A < L) && (priority_inversion_changes_at A
                || task_rbf_changes_at A
                || bound_on_total_hep_workload_changes_at A).

  (** Let [R] be a value 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 [R >= F + (task cost - task lock-in service)]. *)
  Variable R : duration.
  Hypothesis H_R_is_maximum :
    forall (A : duration),
      is_in_search_space A ->
      exists (F : duration),
        A + F >= priority_inversion_bound A
                + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
                + bound_on_athep_workload ts tsk  A (A + F) /\
        R >= F + (task_cost tsk - task_rtct tsk).


  (** Finally, we define the interference bound function
      ([task_IBF]). [task_IBF] bounds the interference if tasks are
      sequential. Since tasks are sequential, we exclude interference
      from other jobs of the same task. For EDF, we define [task_IBF]
      as the sum of the priority interference bound and the
      higher-or-equal-priority workload. *)
  Let task_IBF (A R : duration) :=
    priority_inversion_bound A + bound_on_athep_workload ts tsk A R.

  (** ** Filling Out Hypothesis Of Abstract RTA Theorem *)
  (** In this section we prove that all hypotheses necessary to use
      the abstract theorem are satisfied. *)
  Section FillingOutHypothesesOfAbstractRTATheorem.

    (** First, we prove that [task_IBF] is indeed a valid bound on the
        cumulative task interference. *)
    Lemma instantiated_task_interference_is_bounded :
      task_interference_is_bounded_by arr_seq sched tsk task_IBF.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
task_interference_is_bounded_by arr_seq sched tsk
  task_IBF
    Proof.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
task_interference_is_bounded_by arr_seq sched tsk
  task_IBF
      move => t1 t2 R2 j ARR TSK BUSY LT NCOMPL A OFF.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
A: nat
OFF: relative_arrival_time_of_job_is_A sched j A
cumul_cond_interference (nonself arr_seq sched) j t1
  (t1 + R2) <= task_IBF A R2
      move: (OFF _ _ BUSY) => EQA; subst A.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
cumul_cond_interference (nonself arr_seq sched) j t1
  (t1 + R2) <= task_IBF (job_arrival j - t1) R2
      move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
ZERO: job_cost j = 0
cumul_cond_interference (nonself arr_seq sched) j t1
  (t1 + R2) <= task_IBF (job_arrival j - t1) R2
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
cumul_cond_interference 
  (nonself arr_seq sched) j t1 
  (t1 + R2) <= 
task_IBF (job_arrival j - t1) R2
      -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
ZERO: job_cost j = 0
cumul_cond_interference (nonself arr_seq sched) j t1
  (t1 + R2) <= task_IBF (job_arrival j - t1) R2 exfalso; move: NCOMPL => /negP COMPL; apply: COMPL.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
ZERO: job_cost j = 0
completed_by sched j (t1 + R2)
        by rewrite /completed_by /completed_by ZERO.
      -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
cumul_cond_interference (nonself arr_seq sched) j t1
  (t1 + R2) <= task_IBF (job_arrival j - t1) R2 rewrite -/(cumul_task_interference _ _ _ _ _).
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
cumul_task_interference arr_seq sched j t1 (t1 + R2) <=
task_IBF (job_arrival j - t1) R2
        rewrite (leqRW (cumulative_task_interference_split _ _ _ _ _ _ _ _ _ _ _ _ _)) //=.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
cumulative_priority_inversion arr_seq sched j t1
  (t1 + R2) +
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 (t1 + R2) <=
task_IBF (job_arrival j - t1) R2
        rewrite /I leq_add //; first exact: cumulative_priority_inversion_is_bounded.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 (t1 + R2) <=
bound_on_athep_workload ts tsk (job_arrival j - t1) R2
        eapply leq_trans; first exact: cumulative_interference_is_bounded_by_total_service.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
service_of_jobs sched (another_task_hep_job^~ j)
  (arrivals_between arr_seq t1 (t1 + R2)) t1 (t1 + R2) <=
bound_on_athep_workload ts tsk (job_arrival j - t1) R2
        eapply leq_trans; first exact: service_of_jobs_le_workload.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
workload_of_jobs (another_task_hep_job^~ j)
  (arrivals_between arr_seq t1 (t1 + R2)) <=
bound_on_athep_workload ts tsk (job_arrival j - t1) R2
        eapply leq_trans.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
workload_of_jobs (another_task_hep_job^~ j)
  (arrivals_between arr_seq t1 (t1 + R2)) <= ?n
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
?n <=
bound_on_athep_workload ts tsk (job_arrival j - t1) R2
        +
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
workload_of_jobs (another_task_hep_job^~ j)
  (arrivals_between arr_seq t1 (t1 + R2)) <= ?n eapply reorder_summation.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
forall x : Job,
x \in arrivals_between arr_seq t1 (t1 + R2) ->
hep_job x j -> job_task x \in ?ys
          move => j' IN _.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
j': Job
IN: j' \in arrivals_between arr_seq t1 (t1 + R2)
job_task j' \in ?ys
          apply H_all_jobs_from_taskset.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
j': Job
IN: j' \in arrivals_between arr_seq t1 (t1 + R2)
arrives_in arr_seq j'
          eapply in_arrivals_implies_arrived.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
j': Job
IN: j' \in arrivals_between arr_seq t1 (t1 + R2)
j' \in arrivals_between arr_seq ?t1 ?t2
          exact IN.
        +
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: 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 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
\sum_(y <- ts | y != job_task j)
   \sum_(x <- arrivals_between arr_seq t1 (t1 + R2) | 
   (hep_job^~ j) x && (job_task x == y)) job_cost x <=
bound_on_athep_workload ts tsk (job_arrival j - t1) R2 move : TSK => /eqP TSK.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: nat
j: Job
ARR: arrives_in arr_seq j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
TSK: job_task j = tsk
\sum_(y <- ts | y != job_task j)
   \sum_(x <- arrivals_between arr_seq t1 (t1 + R2) | 
   hep_job x j && (job_task x == y)) job_cost x <=
bound_on_athep_workload ts tsk (job_arrival j - t1) R2
          rewrite TSK.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: nat
j: Job
ARR: arrives_in arr_seq j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
TSK: job_task j = tsk
\sum_(y <- ts | y != tsk)
   \sum_(x <- arrivals_between arr_seq t1 (t1 + R2) | 
   hep_job x j && (job_task x == y)) job_cost x <=
bound_on_athep_workload ts tsk (job_arrival j - t1) R2
          apply: sum_of_workloads_is_at_most_bound_on_total_hep_workload => //.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
t1, t2: instant
R2: nat
j: Job
ARR: arrives_in arr_seq j
BUSY: definitions.busy_interval sched j t1 t2
LT: t1 + R2 < t2
NCOMPL: ~~ completed_by sched j (t1 + R2)
OFF: relative_arrival_time_of_job_is_A sched j
  (job_arrival j - t1)
POS: 0 < job_cost j
TSK: job_task j = tsk
job_of_task tsk j
          by apply /eqP.
    Qed.

      (** Finally, we show that there exists a solution for the response-time recurrence. *)
    Section SolutionOfResponseTimeReccurenceExists.

      (** To rule out pathological cases with the concrete search
          space, we assume that the task cost is positive and the
          arrival curve is non-pathological. *)
      Hypothesis H_task_cost_pos : 0 < task_cost tsk.
      Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.

      (** Given any job [j] of task [tsk] that arrives exactly [A] units
          after the beginning of the busy interval, the bound of the
          total interference incurred by [j] within an interval of
          length [Δ] is equal to [task_rbf (A + ε) - task_cost tsk +
          task_IBF(A, Δ)]. *)
      Let total_interference_bound (A Δ : duration) :=
        task_rbf (A + ε) - task_cost tsk + task_IBF A Δ.

      (** Next, consider any [A] from the search space (in the abstract sense). *)
      Variable A : duration.
      Hypothesis H_A_is_in_abstract_search_space :
        search_space.is_in_search_space L total_interference_bound A.

      (** We prove that A is also in the concrete search space. *)
      Lemma A_is_in_concrete_search_space:
        is_in_search_space A.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
is_in_search_space A
      Proof.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
is_in_search_space A
        move: H_A_is_in_abstract_search_space => [-> | [/andP [POSA LTL] [x [LTx INSP2]]]]; apply/andP; split => //.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
priority_inversion_changes_at 0
|| task_rbf_changes_at 0
|| bound_on_total_hep_workload_changes_at 0
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
priority_inversion_changes_at A
|| task_rbf_changes_at A
|| bound_on_total_hep_workload_changes_at A
        {
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
priority_inversion_changes_at 0
|| task_rbf_changes_at 0
|| bound_on_total_hep_workload_changes_at 0 apply/orP; left; apply/orP; right.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
task_rbf_changes_at 0
          rewrite /task_rbf_changes_at /task_rbf /rbf task_rbf_0_zero // eq_sym -lt0n add0n.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
0 < task_request_bound_function tsk 1
          by apply task_rbf_epsilon_gt_0 => //.
        }
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
priority_inversion_changes_at A
|| task_rbf_changes_at A
|| bound_on_total_hep_workload_changes_at A
        {
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
priority_inversion_changes_at A
|| task_rbf_changes_at A
|| bound_on_total_hep_workload_changes_at A apply contraT; rewrite !negb_or => /andP [/andP [/negPn/eqP PI /negPn/eqP RBF]  WL].
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
false
          exfalso; apply INSP2.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
total_interference_bound (A - 1) x =
total_interference_bound A x
          rewrite /total_interference_bound subnK // RBF.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
task_rbf (A + 1) - task_cost tsk + task_IBF (A - 1) x =
task_rbf (A + 1) - task_cost tsk + task_IBF A x
          apply /eqP; rewrite eqn_add2l /task_IBF PI eqn_add2l.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
bound_on_athep_workload ts tsk (A - 1) x ==
bound_on_athep_workload ts tsk A x
          rewrite /bound_on_athep_workload subnK //.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
\sum_(tsk_o <- ts | tsk_o != tsk)
   task_request_bound_function tsk_o
     (minn
        (A + task_deadline tsk - task_deadline tsk_o)
        x) ==
\sum_(tsk_o <- ts | tsk_o != tsk)
   task_request_bound_function tsk_o
     (minn
        (A + 1 + task_deadline tsk -
         task_deadline tsk_o) x)
          apply /eqP; rewrite big_seq_cond [RHS]big_seq_cond.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
\sum_(i <- ts | (i \in ts) && (i != tsk))
   task_request_bound_function i
     (minn (A + task_deadline tsk - task_deadline i) x) =
\sum_(i <- ts | (i \in ts) && (i != tsk))
   task_request_bound_function i
     (minn
        (A + 1 + task_deadline tsk - task_deadline i)
        x)
          apply eq_big => // tsk_i /andP [TS OTHER].
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
task_request_bound_function tsk_i
  (minn (A + task_deadline tsk - task_deadline tsk_i)
     x) =
task_request_bound_function tsk_i
  (minn
     (A + 1 + task_deadline tsk - task_deadline tsk_i)
     x)
          fold (D tsk) (D tsk_i).
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
task_request_bound_function tsk_i
  (minn (A + D tsk - D tsk_i) x) =
task_request_bound_function tsk_i
  (minn (A + 1 + D tsk - D tsk_i) x)
          move: WL; rewrite /bound_on_total_hep_workload_changes_at => /hasPn WL.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: {in ts,
  forall x : Task,
  ~~
  ((tsk != x) &&
   (rbf x (A + D tsk - D x)
    != rbf x (A + 1 + D tsk - D x)))}
task_request_bound_function tsk_i
  (minn (A + D tsk - D tsk_i) x) =
task_request_bound_function tsk_i
  (minn (A + 1 + D tsk - D tsk_i) x)
          move: {WL} (WL tsk_i TS) =>  /nandP [/negPn/eqP EQ|/negPn/eqP WL];
            first by move: OTHER; rewrite EQ => /neqP.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
task_request_bound_function tsk_i
  (minn (A + D tsk - D tsk_i) x) =
task_request_bound_function tsk_i
  (minn (A + 1 + D tsk - D tsk_i) x)
          case: (ltngtP (A + ε + D tsk - D tsk_i) x) => [ltn_x|gtn_x|eq_x]; rewrite /minn.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
ltn_x: A + 1 + D tsk - D tsk_i < x
task_request_bound_function tsk_i
  (if A + D tsk - D tsk_i < x
   then A + D tsk - D tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i)
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
gtn_x: x < A + 1 + D tsk - D tsk_i
task_request_bound_function tsk_i
  (if A + D tsk - D tsk_i < x
   then A + D tsk - D tsk_i
   else x) = 
task_request_bound_function tsk_i x
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
eq_x: A + 1 + D tsk - D tsk_i = x
task_request_bound_function tsk_i
  (if A + D tsk - D tsk_i < x
   then A + D tsk - D tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i)
          {
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
ltn_x: A + 1 + D tsk - D tsk_i < x
task_request_bound_function tsk_i
  (if A + D tsk - D tsk_i < x
   then A + D tsk - D tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i) by rewrite ifT //; lia. }
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
gtn_x: x < A + 1 + D tsk - D tsk_i
task_request_bound_function tsk_i
  (if A + D tsk - D tsk_i < x
   then A + D tsk - D tsk_i
   else x) = task_request_bound_function tsk_i x
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
eq_x: A + 1 + D tsk - D tsk_i = x
task_request_bound_function tsk_i
  (if A + D tsk - D tsk_i < x
   then A + D tsk - D tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i)
          {
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
gtn_x: x < A + 1 + D tsk - D tsk_i
task_request_bound_function tsk_i
  (if A + D tsk - D tsk_i < x
   then A + D tsk - D tsk_i
   else x) = task_request_bound_function tsk_i x rewrite ifF //.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
gtn_x: x < A + 1 + D tsk - D tsk_i
(A + D tsk - D tsk_i < x) = false
            by move: gtn_x; rewrite leq_eqVlt  => /orP [/eqP EQ|LEQ]; lia. }
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
eq_x: A + 1 + D tsk - D tsk_i = x
task_request_bound_function tsk_i
  (if A + D tsk - D tsk_i < x
   then A + D tsk - D tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i)
          {
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
eq_x: A + 1 + D tsk - D tsk_i = x
task_request_bound_function tsk_i
  (if A + D tsk - D tsk_i < x
   then A + D tsk - D tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i) case: (A + D tsk - D tsk_i < x).
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
eq_x: A + 1 + D tsk - D tsk_i = x
task_request_bound_function tsk_i
  (A + D tsk - D tsk_i) =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i)
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
eq_x: A + 1 + D tsk - D tsk_i = x
task_request_bound_function tsk_i x =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i)
            -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
eq_x: A + 1 + D tsk - D tsk_i = x
task_request_bound_function tsk_i
  (A + D tsk - D tsk_i) =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i) by rewrite -/(rbf _) WL.
            -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: total_interference_bound (A - 1) x <>
total_interference_bound A x
PI: priority_inversion_bound (A - 1) =
priority_inversion_bound A
RBF: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i (A + D tsk - D tsk_i) =
rbf tsk_i (A + 1 + D tsk - D tsk_i)
eq_x: A + 1 + D tsk - D tsk_i = x
task_request_bound_function tsk_i x =
task_request_bound_function tsk_i
  (A + 1 + D tsk - D tsk_i) by rewrite eq_x. } }
      Qed.

      (** Then, there exists solution for response-time recurrence (in the abstract sense). *)
      Corollary correct_search_space:
        exists F,
          A + F >= task_rbf (A + ε) - (task_cost tsk - task_rtct tsk) + task_IBF A (A + F) /\
          R >= F + (task_cost tsk - task_rtct tsk).
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
exists F : nat,
  task_rbf (A + 1) - (task_cost tsk - task_rtct tsk) +
  task_IBF A (A + F) <= A + F /\
  F + (task_cost tsk - task_rtct tsk) <= R
      Proof.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
exists F : nat,
  task_rbf (A + 1) - (task_cost tsk - task_rtct tsk) +
  task_IBF A (A + F) <= A + F /\
  F + (task_cost tsk - task_rtct tsk) <= R
        edestruct H_R_is_maximum as [F [FIX NEQ]]; first by apply A_is_in_concrete_search_space.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
F: duration
FIX: priority_inversion_bound A +
(task_rbf (A + 1) -
 (task_cost tsk - task_rtct tsk)) +
bound_on_athep_workload ts tsk A (A + F) <=
A + F
NEQ: F + (task_cost tsk - task_rtct tsk) <= R
exists F : nat,
  task_rbf (A + 1) - (task_cost tsk - task_rtct tsk) +
  task_IBF A (A + F) <= A + F /\
  F + (task_cost tsk - task_rtct tsk) <= R
        exists F; split=> [|//].
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
F: duration
FIX: priority_inversion_bound A +
(task_rbf (A + 1) -
 (task_cost tsk - task_rtct tsk)) +
bound_on_athep_workload ts tsk A (A + F) <=
A + F
NEQ: F + (task_cost tsk - task_rtct tsk) <= R
task_rbf (A + 1) - (task_cost tsk - task_rtct tsk) +
task_IBF A (A + F) <= A + F
        rewrite -{2}(leqRW FIX).
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
total_interference_bound:= fun A Δ : duration =>
task_rbf (A + 1) -
task_cost tsk + 
task_IBF A Δ: duration -> duration -> nat
A: duration
H_A_is_in_abstract_search_space: search_space.is_in_search_space
  L
  total_interference_bound
  A
F: duration
FIX: priority_inversion_bound A +
(task_rbf (A + 1) -
 (task_cost tsk - task_rtct tsk)) +
bound_on_athep_workload ts tsk A (A + F) <=
A + F
NEQ: F + (task_cost tsk - task_rtct tsk) <= R
task_rbf (A + 1) - (task_cost tsk - task_rtct tsk) +
task_IBF A (A + F) <=
priority_inversion_bound A +
(task_rbf (A + 1) - (task_cost tsk - task_rtct tsk)) +
bound_on_athep_workload ts tsk A (A + F)
        by rewrite addnA [_ + priority_inversion_bound A]addnC -!addnA.
      Qed.

      End SolutionOfResponseTimeReccurenceExists.

  End FillingOutHypothesesOfAbstractRTATheorem.

  (** ** Final Theorem *)
  (** Based on the properties established above, we apply the abstract
      analysis framework to infer that [R] is a response-time bound for
      [tsk]. *)
  Theorem uniprocessor_response_time_bound_edf:
    task_response_time_bound arr_seq sched tsk R.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
task_response_time_bound arr_seq sched tsk R
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
task_response_time_bound arr_seq sched tsk R
    move => js ARRs TSKs.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
job_response_time_bound sched js R
    move: (posnP (@job_cost _ Cost js)) => [ZERO|POS].
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
ZERO: job_cost js = 0
job_response_time_bound sched js R
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
job_response_time_bound sched js R
    {
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
ZERO: job_cost js = 0
job_response_time_bound sched js R by rewrite /job_response_time_bound /completed_by ZERO. }
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
job_response_time_bound sched js R
    eapply uniprocessor_response_time_bound_seq with
      (task_IBF := task_IBF) (L := L) => //.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
work_conserving arr_seq sched
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
sequential_tasks arr_seq sched
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
interference_and_workload_consistent_with_sequential_tasks
  arr_seq sched tsk
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
busy_intervals_are_bounded_by arr_seq sched tsk L
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
task_interference_is_bounded_by arr_seq sched tsk
  task_IBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
forall A : duration,
search_space.is_in_search_space L
  (fun A0 Δ : duration =>
   task_request_bound_function tsk (A0 + 1) -
   task_cost tsk + 
   task_IBF A0 Δ) A ->
exists F : duration,
  task_request_bound_function tsk (A + 1) -
  (task_cost tsk - task_rtct tsk) + 
  task_IBF A (A + F) <= 
  A + F /\ 
  F + (task_cost tsk - task_rtct tsk) <= R
    -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
work_conserving arr_seq sched exact: instantiated_i_and_w_are_coherent_with_schedule.
    -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
sequential_tasks arr_seq sched exact: EDF_implies_sequential_tasks.
    -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
interference_and_workload_consistent_with_sequential_tasks
  arr_seq sched tsk exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
    -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
busy_intervals_are_bounded_by arr_seq sched tsk L exact: instantiated_busy_intervals_are_bounded.
    -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
task_interference_is_bounded_by arr_seq sched tsk
  task_IBF exact: instantiated_task_interference_is_bounded.
    -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
H4: JobPreemptable Job
D:= [eta task_deadline]: Task -> duration
EDF:= edf.EDF Job: JLFP_policy Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_sched_valid: valid_schedule sched arr_seq
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched EDF
work_conserving_ab:= work_conserving arr_seq sched: Prop
work_conserving_cl:= work_conserving.work_conserving
  arr_seq sched: Prop
H_work_conserving: work_conserving_cl
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
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
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf:= rbf tsk: duration -> nat
total_rbf:= total_request_bound_function ts: duration -> nat
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
L: duration
H_L_positive: 0 < L
H_fixed_point: L = total_rbf L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space A ->
exists F : duration,
  priority_inversion_bound A +
  (task_rbf (A + 1) -
   (task_cost tsk - task_rtct tsk)) +
  bound_on_athep_workload ts tsk A
    (A + F) <= 
  A + F /\
  F + (task_cost tsk - task_rtct tsk) <=
  R
task_IBF:= fun A R : duration =>
priority_inversion_bound A +
bound_on_athep_workload ts tsk A R: duration -> duration -> nat
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
forall A : duration,
search_space.is_in_search_space L
  (fun A0 Δ : duration =>
   task_request_bound_function tsk (A0 + 1) -
   task_cost tsk + task_IBF A0 Δ) A ->
exists F : duration,
  task_request_bound_function tsk (A + 1) -
  (task_cost tsk - task_rtct tsk) + task_IBF A (A + F) <=
  A + F /\ F + (task_cost tsk - task_rtct tsk) <= R exact: correct_search_space.
  Qed.

End AbstractRTAforEDFwithArrivalCurves.