Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[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.facts.model.restricted_supply.schedule.
Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.
Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.edf.
Require Export prosa.analysis.abstract.restricted_supply.search_space.edf.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.facts.priority.edf.
Require Export prosa.analysis.facts.blocking_bound.edf.
Require Export prosa.analysis.facts.workload.edf_athep_bound.
Require Export prosa.analysis.definitions.sbf.busy.

(** * RTA for Fully Non-Preemptive EDF Scheduling on Restricted-Supply Uniprocessors *)

(** In the following, we derive a response-time analysis for EDF
    schedulers, assuming a workload of sporadic real-time tasks
    characterized by arbitrary arrival curves executing upon a
    uniprocessor with arbitrary supply restrictions. To this end, we
    instantiate the _abstract Sequential Restricted-Supply
    Response-Time Analysis_ (aRSA) as provided in the
    [prosa.analysis.abstract.restricted_supply] module. *)
Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.

  (** ** Defining the System Model *)

  (** Before any formal claims can be stated, an initial setup is
      needed to define the system model under consideration. To this
      end, we next introduce and define the following notions using
      Prosa's standard definitions and behavioral semantics:

      - processor model,
      - tasks, jobs, and their parameters,
      - the sequence of job arrivals,
      - worst-case execution time (WCET) and the absence of self-suspensions,
      - the set of tasks under analysis,
      - the task under analysis, and, finally,
      - an arbitrary schedule of the task set. *)

  (** *** Processor Model *)

  (** Consider a restricted-supply uniprocessor model, ... *)
  #[local] Existing Instance rs_processor_state.

  (** ... where the minimum amount of supply is lower-bounded via a
      monotone unit-supply-bound function [SBF]. *)
  Context {SBF : SupplyBoundFunction}.
  Hypothesis H_SBF_monotone : sbf_is_monotone SBF.
  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.

  (** *** Tasks and Jobs  *)

  (** Consider any type of tasks, each characterized by a WCET
      [task_cost], relative deadline [task_deadline], and an arrival
      curve [max_arrivals], ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.
  Context `{MaxArrivals Task}.

  (** ... and any type of jobs associated with these tasks, where each
      job has a task [job_task], a cost [job_cost], and an arrival
      time [job_arrival]. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobCost Job}.
  Context `{JobArrival Job}.

  (** Furthermore, assume that jobs and tasks are fully non-preemptive. *)
  #[local] Existing Instance fully_nonpreemptive_job_model.
  #[local] Existing Instance fully_nonpreemptive_task_model.
  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.

  (** *** The Job Arrival Sequence *)

  (** Consider any arrival sequence [arr_seq] with consistent, non-duplicate arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** *** Absence of Self-Suspensions and WCET Compliance *)

  (** 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.

  (** We further require that a job's cost cannot exceed its task's stated WCET. *)
  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.

  (** *** The Task Set *)

  (** We consider an arbitrary task set [ts] ... *)
  Variable ts : seq Task.

  (** ... and assume that all jobs stem from tasks in this task set. *)
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

  (** We assume that [max_arrivals] is a family of valid arrival
      curves that constrains the arrival sequence [arr_seq], i.e., for
      any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
      bound of [tsk], and ... *)
  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

  (** ... (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *)
  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.

  (** *** The Task Under Analysis *)

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

  (** *** The Schedule *)

  (** Finally, consider any non-preemptive, work-conserving, valid
      restricted-supply uni-processor schedule of the given arrival
      sequence [arr_seq] (and hence the given task set [ts]) ... *)
  Variable sched : schedule (rs_processor_state Job).
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
  Hypothesis H_work_conserving : work_conserving arr_seq sched.
  Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.

  (** ... and assume that the schedule respects the EDF policy. *)
  Hypothesis H_respects_policy :
    respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

  (** Last but not least, we assume that [SBF] properly characterizes
      all busy intervals (w.r.t. task [tsk]) in [sched]. That is, (1)
      [SBF 0 = 0] and (2) for any duration [Δ], at least [SBF Δ]
      supply is available in any busy-interval prefix of length
      [Δ]. *)
  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.

  (** ** Workload Abbreviation *)

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

  (** We introduce [task_rbf] as an abbreviation
      for the task request bound function of task [tsk]. *)
  Let task_rbf := task_request_bound_function tsk.

  (** ** Length of Busy Interval *)

  (** The next step is to establish a bound on the maximum busy-window
      length, which aRTA requires to be given. *)

  (** To this end, let [L] be any positive constant such that ...  *)
  Variable L : duration.
  Hypothesis H_L_positive : 0 < L.

  (** ... [L] satisfies a fixed-point recurrence for the
      busy-interval-length bound (i.e., [total_RBF ts L <= SBF L] ... *)
  Hypothesis H_fixed_point : total_request_bound_function ts L <= SBF L.

  (** ... and [SBF L] bounds [longest_busy_interval_with_pi ts tsk]. *)
  Hypothesis H_L_bounds_bi_with_pi :
    longest_busy_interval_with_pi ts tsk <= SBF L.


  (** ** Response-Time Bound *)

  (** Having established all necessary preliminaries, it is finally
      time to state the claimed response-time bound [R].

      A value [R] is a response-time bound if, for any given offset
      [A] in the search space, the response-time bound recurrence has
      a solution [F] not exceeding [R]. *)
  Variable R : duration.
  Hypothesis H_R_is_maximum :
    forall (A : duration),
      is_in_search_space ts tsk L A ->
      exists (F : duration),
        A <= F <= A + R
        /\ blocking_bound ts tsk A
          + (task_rbf (A + ε) - (task_cost tsk - ε))
          + bound_on_athep_workload ts tsk A F
          <= SBF F
        /\ SBF F + (task_cost tsk - ε) <= SBF (A + R).

  (** Finally, using the sequential variant of abstract
      restricted-supply analysis, we establish that any such [R] is a
      sound response-time bound for the concrete model of
      fully-nonpreemptive EDF scheduling with arbitrary supply
      restrictions. *)
  
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
task_response_time_bound arr_seq sched tsk R

  
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
task_response_time_bound arr_seq sched tsk R

    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
job_response_time_bound sched js R

    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
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

    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
job_response_time_bound sched js R

    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
job_response_time_bound sched js R

    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
definitions.work_conserving arr_seq sched
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
sequential_tasks arr_seq sched
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
interference_and_workload_consistent_with_sequential_tasks
  arr_seq sched tsk
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
busy_intervals_are_bounded_by arr_seq sched tsk L
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
busy_sbf.valid_busy_sbf arr_seq sched tsk SBF
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
task_intra_interference_is_bounded_by arr_seq sched
  tsk ?task_intra_IBF
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
forall A : duration,
search_space.is_in_search_space L
  (fun A0 Δ : duration =>
   task_request_bound_function tsk (A0 + 1) -
   task_cost tsk + ?task_intra_IBF A0 Δ) A ->
exists F : duration,
  F <= A + R /\
  task_request_bound_function tsk (A + 1) -
  (task_cost tsk - task_rtct tsk) +
  ?task_intra_IBF A F <= 
  SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)

    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
definitions.work_conserving arr_seq sched
 exact: instantiated_i_and_w_are_coherent_with_schedule.
    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
sequential_tasks arr_seq sched
 exact: EDF_implies_sequential_tasks.
    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
interference_and_workload_consistent_with_sequential_tasks
  arr_seq sched tsk
 exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
busy_intervals_are_bounded_by arr_seq sched tsk L
 apply: busy_intervals_are_bounded_rs_edf => //.
    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
busy_sbf.valid_busy_sbf arr_seq sched tsk SBF
 
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
job_of_task tsk j /\
definitions.busy_interval_prefix sched j t1 t2 ->
(fun (j0 : Job) (t3 t4 : instant) =>
 job_of_task tsk j0 /\
 busy_interval_prefix arr_seq sched j0 t3 t4) j t1 t2

      
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
_j_: Job
_t1_, _t2_: instant
_Hyp_: arrives_in arr_seq _j_
_a_: job_of_task tsk _j_
_b_: definitions.busy_interval_prefix sched _j_ _t1_
  _t2_
busy_interval_prefix arr_seq sched _j_ _t1_ _t2_

      by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
task_intra_interference_is_bounded_by arr_seq sched
  tsk ?task_intra_IBF
 
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
athep_workload_is_bounded arr_seq sched tsk ?Goal2
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
service_inversion_is_bounded_by arr_seq sched tsk
  ?Goal0

      
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
athep_workload_is_bounded arr_seq sched tsk ?Goal2
 by (apply: bound_on_athep_workload_is_valid; try apply H_fixed_point) => //.
      
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
service_inversion_is_bounded_by arr_seq sched tsk
  ?Goal0
 
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
jo: Job
t1, t2: instant
ARRo: arrives_in arr_seq jo
TSKo: job_of_task tsk jo
BUSYo: busy_interval_prefix arr_seq sched jo t1 t2
max_lp_nonpreemptive_segment arr_seq jo t1 <=
?Goal0 (job_arrival jo - t1)

        by apply: nonpreemptive_segments_bounded_by_blocking => //.
    
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
forall A : duration,
search_space.is_in_search_space L
  (fun A0 Δ : duration =>
   task_request_bound_function tsk (A0 + 1) -
   task_cost tsk +
   task_intra_IBF (blocking_bound ts tsk)
     (bound_on_athep_workload ts tsk) A0 Δ) A ->
exists F : duration,
  F <= A + R /\
  task_request_bound_function tsk (A + 1) -
  (task_cost tsk - task_rtct tsk) +
  task_intra_IBF (blocking_bound ts tsk)
    (bound_on_athep_workload ts tsk) A F <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
 
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
A: duration
SP: search_space.is_in_search_space L
  (fun A Δ : duration =>
   task_request_bound_function tsk (A + 1) -
   task_cost tsk +
   task_intra_IBF (blocking_bound ts tsk)
     (bound_on_athep_workload ts tsk) A Δ) A
is_in_search_space ts tsk L A
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
A: duration
SP: search_space.is_in_search_space L
  (fun A Δ : duration =>
   task_request_bound_function tsk (A + 1) -
   task_cost tsk +
   task_intra_IBF (blocking_bound ts tsk)
     (bound_on_athep_workload ts tsk) A Δ) A
forall x : duration,
A <= x <= A + R /\
blocking_bound ts tsk A +
(task_rbf (A + 1) - (task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A x <= 
SBF x /\ SBF x + (task_cost tsk - 1) <= SBF (A + R) ->
exists F : duration,
  F <= A + R /\
  task_request_bound_function tsk (A + 1) -
  (task_cost tsk - task_rtct tsk) +
  task_intra_IBF (blocking_bound ts tsk)
    (bound_on_athep_workload ts tsk) A F <= 
  SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)

      
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
A: duration
SP: search_space.is_in_search_space L
  (fun A Δ : duration =>
   task_request_bound_function tsk (A + 1) -
   task_cost tsk +
   task_intra_IBF (blocking_bound ts tsk)
     (bound_on_athep_workload ts tsk) A Δ) A
is_in_search_space ts tsk L A
 by apply: search_space_sub => //.
      
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
A: duration
SP: search_space.is_in_search_space L
  (fun A Δ : duration =>
   task_request_bound_function tsk (A + 1) -
   task_cost tsk +
   task_intra_IBF (blocking_bound ts tsk)
     (bound_on_athep_workload ts tsk) A Δ) A
forall x : duration,
A <= x <= A + R /\
blocking_bound ts tsk A +
(task_rbf (A + 1) - (task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A x <= SBF x /\
SBF x + (task_cost tsk - 1) <= SBF (A + R) ->
exists F : duration,
  F <= A + R /\
  task_request_bound_function tsk (A + 1) -
  (task_cost tsk - task_rtct tsk) +
  task_intra_IBF (blocking_bound ts tsk)
    (bound_on_athep_workload ts tsk) A F <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
 
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
A: duration
SP: search_space.is_in_search_space L
  (fun A Δ : duration =>
   task_request_bound_function tsk (A + 1) -
   task_cost tsk +
   task_intra_IBF (blocking_bound ts tsk)
     (bound_on_athep_workload ts tsk) A Δ) A
F: duration
LE: F <= A + R
FIX1: blocking_bound ts tsk A +
(task_rbf (A + 1) - (task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A F <= 
SBF F
FIX2: SBF F + (task_cost tsk - 1) <= SBF (A + R)
task_request_bound_function tsk (A + 1) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF (blocking_bound ts tsk)
  (bound_on_athep_workload ts tsk) A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R)

        
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobCost Job
H4: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
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
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule (rs_processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_nonpreemptive_sched: nonpreemptive_schedule sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
D:= [eta task_deadline]: Task -> duration
task_rbf:= task_request_bound_function tsk: duration -> nat
L: duration
H_L_positive: 0 < L
H_fixed_point: total_request_bound_function ts L <=
SBF L
H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
  ts tsk <= SBF L
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts tsk L A ->
exists F : duration,
  A <= F <= A + R /\
  blocking_bound ts tsk A +
  (task_rbf (A + 1) -
   (task_cost tsk - 1)) +
  bound_on_athep_workload ts tsk A F <=
  SBF F /\
  SBF F + (task_cost tsk - 1) <=
  SBF (A + R)
js: Job
ARRs: arrives_in arr_seq js
TSKs: job_of_task tsk js
POS: 0 < job_cost js
READ: work_bearing_readiness arr_seq sched
VPR: valid_preemption_model arr_seq sched
A: duration
SP: search_space.is_in_search_space L
  (fun A Δ : duration =>
   task_request_bound_function tsk (A + 1) -
   task_cost tsk +
   task_intra_IBF (blocking_bound ts tsk)
     (bound_on_athep_workload ts tsk) A Δ) A
F: duration
LE: F <= A + R
FIX1: blocking_bound ts tsk A +
(task_rbf (A + 1) - (task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A F <= 
SBF F
FIX2: SBF F + (task_cost tsk - 1) <= SBF (A + R)
task_request_bound_function tsk (A + 1) -
(task_cost tsk - 1) +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F) <= SBF F /\
SBF F + (task_cost tsk - 1) <= SBF (A + R)

        by split; [rewrite -(leqRW FIX1) /task_rbf | ]; lia.
  Qed.

End RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.