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

(** * Concrete to Abstract Fixpoint Reduction *)

(** In this file, we show that a solution to a concrete fixpoint
    equation under the FIFO policy implies a solution to the
    abstract fixpoint equation required by aRSA. *)
Section ConcreteToAbstractFixpointReduction.

  (** Consider any type of tasks, each characterized by a WCET
      [task_cost], an arrival curve [max_arrivals], a
      run-to-completion threshold [task_rtct], and a bound on the
      task's maximum non-preemptive segment
      [task_max_nonpreemptive_segment] ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{MaxArrivals Task}.
  Context `{TaskRunToCompletionThreshold Task}.
  Context `{TaskMaxNonpreemptiveSegment Task}.

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

  (** Consider any processor model ... *)
  Context `{PState : ProcessorState Job}.

  (** ... where the minimum amount of supply is defined 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.

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

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

  (** Consider any arrival sequence ... *)
  Variable arr_seq : arrival_sequence Job.

  (** ... and assume that [max_arrivals] defines a valid arrival curve
      for each task. *)
  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.

  (** Consider any schedule. *)
  Variable sched : schedule PState.

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

  (** We assume that [tsk] is described by a valid task
      run-to-completion threshold_ *)
  Hypothesis H_valid_run_to_completion_threshold :
    valid_task_run_to_completion_threshold arr_seq tsk.

  (** Let [L] be an arbitrary positive constant. Typically, [L]
      denotes an upper bound on the length of a busy interval of a job
      of [tsk]. In this file, however, [L] can be any positive
      constant. *)
  Variable L : duration.
  Hypothesis H_L_positive : 0 < L.

  (** To rule out pathological cases with the 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 ε.

  (** For brevity, we define the intra-supply interference bound
      function ([intra_IBF]). Note that in the case of FIFO,
      intra-supply IBF does not depend on the second argument.  *)
  Local Definition intra_IBF (A _Δ : duration) :=
    total_request_bound_function ts (A + ε) - task_cost tsk.

  (** Ultimately, we seek to apply aRSA to prove the correctness of
      the following [R]. *)
  Variable R : duration.
  Hypothesis H_R_is_maximum :
    forall (A : duration),
      is_in_search_space ts L A ->
      exists (F : duration),
        A <= F <= A + R
        /\ total_request_bound_function ts (A + ε) <= SBF F.

  (** However, in order to connect the definition of [R] with aRSA, we
      must first restate the bound in the shape of the abstract
      response-time bound equation that aRSA expects, which we do
      next. *)

  (** We know that:
     - if [A] is in the abstract search space, then it is also in the
       concrete search space; and
     - if [A] is in the concrete search space, then there exists a
       solution that satisfies the inequalities stated in
       [H_R_is_maximum]. Using these facts, we prove that, if [A] is
       in the abstract search space, then there also exists a solution
       [F] to the response-time equation as expected by aRSA. *)
  Lemma soln_abstract_response_time_recurrence :
    forall A : duration,
      abstract.search_space.is_in_search_space L (fifo.IBF ts tsk) A ->
      exists F : duration,
        F <= A + R
        /\ task_rtct tsk + intra_IBF A F <= SBF F
        /\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts
    (A + 1) <= 
  SBF F
forall A : duration,
search_space.is_in_search_space L (fifo.IBF ts tsk) A ->
exists F : duration,
  F <= A + R /\
  task_rtct tsk + intra_IBF A F <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
  Proof.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts
    (A + 1) <= 
  SBF F
forall A : duration,
search_space.is_in_search_space L (fifo.IBF ts tsk) A ->
exists F : duration,
  F <= A + R /\
  task_rtct tsk + intra_IBF A F <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    move => A SP; move: (H_R_is_maximum A) => MAX.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts
    (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
MAX: is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts (A + 1) <=
  SBF F
exists F : duration,
  F <= A + R /\
  task_rtct tsk + intra_IBF A F <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    rewrite /intra_IBF.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts
    (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
MAX: is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts (A + 1) <=
  SBF F
exists F : duration,
  F <= A + R /\
  task_rtct tsk +
  (total_request_bound_function ts (A + 1) -
   task_cost tsk) <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    feed MAX; first by apply: search_space_sub => //.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts
    (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
MAX: exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts (A + 1) <=
  SBF F
exists F : duration,
  F <= A + R /\
  task_rtct tsk +
  (total_request_bound_function ts (A + 1) -
   task_cost tsk) <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    move: MAX => [F' [FE LGL]].
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts
    (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: total_request_bound_function ts (A + 1) <=
SBF F'
exists F : duration,
  F <= A + R /\
  task_rtct tsk +
  (total_request_bound_function ts (A + 1) -
   task_cost tsk) <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    have Leq1 : SBF F' <= SBF (A + R) by apply H_SBF_monotone; lia.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts
    (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: total_request_bound_function ts (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
exists F : duration,
  F <= A + R /\
  task_rtct tsk +
  (total_request_bound_function ts (A + 1) -
   task_cost tsk) <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    have Leq2 : total_request_bound_function ts (A + 1) >= task_cost tsk by apply task_cost_le_sum_rbf => //; lia.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts
    (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: total_request_bound_function ts (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
total_request_bound_function ts (A + 1)
exists F : duration,
  F <= A + R /\
  task_rtct tsk +
  (total_request_bound_function ts (A + 1) -
   task_cost tsk) <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    have Leq3 : task_cost tsk >= task_rtct tsk by apply H_valid_run_to_completion_threshold.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  total_request_bound_function ts
    (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: total_request_bound_function ts (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
total_request_bound_function ts (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
exists F : duration,
  F <= A + R /\
  task_rtct tsk +
  (total_request_bound_function ts (A + 1) -
   task_cost tsk) <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    unfold total_request_bound_function in *.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
exists F : duration,
  F <= A + R /\
  task_rtct tsk +
  (\sum_(tsk <- ts)
      task_request_bound_function tsk (A + 1) -
   task_cost tsk) <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    have [F'' [LE EX]]:
      exists F'',
        0 <= F'' <= A + R
        /\ SBF F'' = SBF (A + R) - (task_cost tsk - task_rtct tsk).
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
exists F'' : nat,
  0 <= F'' <= A + R /\
  SBF F'' =
  SBF (A + R) - (task_cost tsk - task_rtct tsk)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
F'': nat
LE: 0 <= F'' <= A + R
EX: SBF F'' =
SBF (A + R) - (task_cost tsk - task_rtct tsk)
exists F : duration,
  F <= A + R /\
  task_rtct tsk +
  (\sum_(tsk <- ts)
      task_request_bound_function tsk (A + 1) -
   task_cost tsk) <= 
  SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    {
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
exists F'' : nat,
  0 <= F'' <= A + R /\
  SBF F'' =
  SBF (A + R) - (task_cost tsk - task_rtct tsk) apply exists_intermediate_point_leq.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
unit_growth_function SBF
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
0 <= A + R
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
SBF 0 <=
SBF (A + R) - (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
      -
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
unit_growth_function SBF by move=> t; rewrite !addn1; apply H_unit_SBF.
      -
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
0 <= A + R lia.
      -
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
SBF 0 <=
SBF (A + R) - (task_cost tsk - task_rtct tsk) <=
SBF (A + R) apply/andP; split.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
SBF 0 <= SBF (A + R) - (task_cost tsk - task_rtct tsk)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
SBF (A + R) - (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
        +
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
SBF 0 <= SBF (A + R) - (task_cost tsk - task_rtct tsk) rewrite (fst H_valid_SBF); lia.
        +
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
SBF (A + R) - (task_cost tsk - task_rtct tsk) <=
SBF (A + R) lia.
    }
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
F'': nat
LE: 0 <= F'' <= A + R
EX: SBF F'' =
SBF (A + R) - (task_cost tsk - task_rtct tsk)
exists F : duration,
  F <= A + R /\
  task_rtct tsk +
  (\sum_(tsk <- ts)
      task_request_bound_function tsk (A + 1) -
   task_cost tsk) <= SBF F /\
  SBF F + (task_cost tsk - task_rtct tsk) <=
  SBF (A + R)
    exists F''; split; last split.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
F'': nat
LE: 0 <= F'' <= A + R
EX: SBF F'' =
SBF (A + R) - (task_cost tsk - task_rtct tsk)
F'' <= A + R
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
F'': nat
LE: 0 <= F'' <= A + R
EX: SBF F'' =
SBF (A + R) - (task_cost tsk - task_rtct tsk)
task_rtct tsk +
(\sum_(tsk <- ts)
    task_request_bound_function tsk (A + 1) -
 task_cost tsk) <= 
SBF F''
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
F'': nat
LE: 0 <= F'' <= A + R
EX: SBF F'' =
SBF (A + R) - (task_cost tsk - task_rtct tsk)
SBF F'' + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
    +
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
F'': nat
LE: 0 <= F'' <= A + R
EX: SBF F'' =
SBF (A + R) - (task_cost tsk - task_rtct tsk)
F'' <= A + R by move: LE; clear; lia.
    +
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
F'': nat
LE: 0 <= F'' <= A + R
EX: SBF F'' =
SBF (A + R) - (task_cost tsk - task_rtct tsk)
task_rtct tsk +
(\sum_(tsk <- ts)
    task_request_bound_function tsk (A + 1) -
 task_cost tsk) <= SBF F'' by rewrite EX; lia.
    +
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskRunToCompletionThreshold Task
H2: TaskMaxNonpreemptiveSegment Task
Job: JobType
H3: JobTask Job Task
H4: JobCost Job
H5: JobArrival Job
H6: JobPreemptable Job
PState: ProcessorState Job
SBF: SupplyBoundFunction
H_SBF_monotone: sbf_is_monotone SBF
H_unit_SBF: unit_supply_bound_function SBF
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
arr_seq: arrival_sequence Job
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
sched: schedule PState
H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold
  arr_seq tsk
L: duration
H_L_positive: 0 < L
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
R: duration
H_R_is_maximum: forall A : duration,
is_in_search_space ts L A ->
exists F : duration,
  A <= F <= A + R /\
  \sum_(tsk <- ts)
     task_request_bound_function tsk
       (A + 1) <= 
  SBF F
A: duration
SP: search_space.is_in_search_space L
  (fifo.IBF ts tsk) A
F': duration
FE: A <= F' <= A + R
LGL: \sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1) <=
SBF F'
Leq1: SBF F' <= SBF (A + R)
Leq2: task_cost tsk <=
\sum_(tsk <- ts)
   task_request_bound_function tsk (A + 1)
Leq3: task_rtct tsk <= task_cost tsk
F'': nat
LE: 0 <= F'' <= A + R
EX: SBF F'' =
SBF (A + R) - (task_cost tsk - task_rtct tsk)
SBF F'' + (task_cost tsk - task_rtct tsk) <=
SBF (A + R) by rewrite EX; lia.
  Qed.

End ConcreteToAbstractFixpointReduction.