edf.v

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

(** * Abstract Search Space is a Subset of Restricted Supply EDF Search Space *)

(** A response-time analysis usually involves solving the
    response-time equation for various relative arrival times
    (w.r.t. the beginning of the corresponding busy interval) of a job
    under analysis. To reduce the time complexity of the analysis, the
    state of the art uses the notion of a search space. Intuitively,
    this corresponds to all "interesting" arrival offsets that the job
    under analysis might have with regard to the beginning of its busy
    window.

    In this file, we prove that the search space derived from the aRSA
    theorem is a subset of the search space for the EDF scheduling
    policy with restricted supply. In other words, by solving the
    response-time equation for points in the EDF search space, one
    also checks all points in the aRTA search space, which makes EDF
    compatible with aRTA w.r.t. the search space. *)
Section SearchSpaceSubset.

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

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

  (** Let [max_arrivals] be a family of valid arrival curves. *)
  Context `{MaxArrivals Task}.
  Hypothesis H_valid_arrival_curve :
    valid_taskset_arrival_curve ts max_arrivals.

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

  (** Let [L] be an arbitrary positive constant. Normally, [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.

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

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

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

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

  (** Second, we ask whether there exists a task [tsko] from [ts] such
      that [tsko ≠ tsk] and [rbf(tsko, A + D tsk - D tsko) ≠ rbf(tsko,
      A + ε + D tsk - D tsko)]. *)
  Let bound_on_total_hep_workload_changes_at (A : duration) :=
    let new_hep_job_released_by tsko :=
      (tsk != tsko) && (rbf tsko (A + D tsk - D tsko) != rbf tsko ((A + ε) + D tsk - D tsko))
    in has new_hep_job_released_by ts.

  (** Third, we ask whether [blocking_bound (A - ε) ≠ blocking_bound A]. *)
  Let blocking_bound_changes_at (A : duration) :=
    blocking_bound ts tsk (A - ε) != blocking_bound ts tsk A.

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

  (** 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, let us introduce a shorthand for an intra-IBF. The
      abstract search space is derived via intra-IBF. *)
  Let intra_IBF (A F : duration) :=
    rbf tsk (A + ε) - task_cost tsk
    + (blocking_bound ts tsk A + bound_on_athep_workload ts tsk A F).

  (** Then, abstract RTA's standard search space is a subset of the
      computation-oriented version defined above. *)
  Lemma search_space_sub :
    forall A,
      abstract.search_space.is_in_search_space L intra_IBF A ->
      is_in_search_space A.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
forall A : nat,
search_space.is_in_search_space L intra_IBF A ->
is_in_search_space A
  Proof.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
forall A : nat,
search_space.is_in_search_space L intra_IBF A ->
is_in_search_space A
    move => A [-> | [/andP [POSA LTL] [x [LTx INSP2]]]]; apply/andP; split => //.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
blocking_bound_changes_at 0 || task_rbf_changes_at 0
|| bound_on_total_hep_workload_changes_at 0
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
blocking_bound_changes_at A || task_rbf_changes_at A
|| bound_on_total_hep_workload_changes_at A
    {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
blocking_bound_changes_at 0 || task_rbf_changes_at 0
|| bound_on_total_hep_workload_changes_at 0 apply/orP; left; apply/orP; right.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
task_rbf_changes_at 0
      rewrite /task_rbf_changes_at /rbf task_rbf_0_zero // eq_sym -lt0n add0n.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
0 < task_request_bound_function tsk 1
      by apply task_rbf_epsilon_gt_0 => //.
    }Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
blocking_bound_changes_at A || task_rbf_changes_at A
|| bound_on_total_hep_workload_changes_at A
    {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
blocking_bound_changes_at A || task_rbf_changes_at A
|| bound_on_total_hep_workload_changes_at A apply contraT; rewrite !negb_or => /andP [/andP [/negPn/eqP PI /negPn/eqP RBF]  WL].Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
false
      exfalso; apply INSP2.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
intra_IBF (A - 1) x = intra_IBF A x
      rewrite /intra_IBF subnK // RBF.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk (A - 1) +
 bound_on_athep_workload ts tsk (A - 1) x) =
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A x)
      apply /eqP; rewrite eqn_add2l PI eqn_add2l.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
bound_on_athep_workload ts tsk (A - 1) x ==
bound_on_athep_workload ts tsk A x
      rewrite /bound_on_athep_workload subnK //.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
\sum_(tsk_o <- ts | tsk_o != tsk)
   task_request_bound_function tsk_o
     (minn
        (A + task_deadline tsk - task_deadline tsk_o)
        x) ==
\sum_(tsk_o <- ts | tsk_o != tsk)
   task_request_bound_function tsk_o
     (minn
        (A + 1 + task_deadline tsk -
         task_deadline tsk_o) x)
      apply /eqP; rewrite big_seq_cond [RHS]big_seq_cond.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
\sum_(i <- ts | (i \in ts) && (i != tsk))
   task_request_bound_function i
     (minn (A + task_deadline tsk - task_deadline i) x) =
\sum_(i <- ts | (i \in ts) && (i != tsk))
   task_request_bound_function i
     (minn
        (A + 1 + task_deadline tsk - task_deadline i)
        x)
      apply eq_big => // tsk_i /andP [TS OTHER].Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
WL: ~~ bound_on_total_hep_workload_changes_at A
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
task_request_bound_function tsk_i
  (minn (A + task_deadline tsk - task_deadline tsk_i)
     x) =
task_request_bound_function tsk_i
  (minn
     (A + 1 + task_deadline tsk - task_deadline tsk_i)
     x)
      move: WL; rewrite /bound_on_total_hep_workload_changes_at /D => /hasPn WL.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: {in ts,
  forall x : Task,
  ~~
  ((tsk != x) &&
   (rbf x
      (A + task_deadline tsk - task_deadline x)
    != rbf x
         (A + 1 + task_deadline tsk -
         task_deadline x)))}
task_request_bound_function tsk_i
  (minn (A + task_deadline tsk - task_deadline tsk_i)
     x) =
task_request_bound_function tsk_i
  (minn
     (A + 1 + task_deadline tsk - task_deadline tsk_i)
     x)
      move: {WL} (WL tsk_i TS) =>  /nandP [/negPn/eqP EQ|/negPn/eqP WL];
                                  first by move: OTHER; rewrite EQ => /neqP.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
task_request_bound_function tsk_i
  (minn (A + task_deadline tsk - task_deadline tsk_i)
     x) =
task_request_bound_function tsk_i
  (minn
     (A + 1 + task_deadline tsk - task_deadline tsk_i)
     x)
      case: (ltngtP (A + ε + task_deadline tsk - task_deadline tsk_i) x) => [ltn_x|gtn_x|eq_x]; rewrite /minn.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
ltn_x: A + 1 + task_deadline tsk -
task_deadline tsk_i < x
task_request_bound_function tsk_i
  (if A + task_deadline tsk - task_deadline tsk_i < x
   then A + task_deadline tsk - task_deadline tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i)
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
gtn_x: x <
A + 1 + task_deadline tsk -
task_deadline tsk_i
task_request_bound_function tsk_i
  (if A + task_deadline tsk - task_deadline tsk_i < x
   then A + task_deadline tsk - task_deadline tsk_i
   else x) = 
task_request_bound_function tsk_i x
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
eq_x: A + 1 + task_deadline tsk - task_deadline tsk_i =
x
task_request_bound_function tsk_i
  (if A + task_deadline tsk - task_deadline tsk_i < x
   then A + task_deadline tsk - task_deadline tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i)
      {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
ltn_x: A + 1 + task_deadline tsk -
task_deadline tsk_i < x
task_request_bound_function tsk_i
  (if A + task_deadline tsk - task_deadline tsk_i < x
   then A + task_deadline tsk - task_deadline tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i) by rewrite ifT //; lia. }Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
gtn_x: x <
A + 1 + task_deadline tsk -
task_deadline tsk_i
task_request_bound_function tsk_i
  (if A + task_deadline tsk - task_deadline tsk_i < x
   then A + task_deadline tsk - task_deadline tsk_i
   else x) = task_request_bound_function tsk_i x
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
eq_x: A + 1 + task_deadline tsk - task_deadline tsk_i =
x
task_request_bound_function tsk_i
  (if A + task_deadline tsk - task_deadline tsk_i < x
   then A + task_deadline tsk - task_deadline tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i)
      {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
gtn_x: x <
A + 1 + task_deadline tsk -
task_deadline tsk_i
task_request_bound_function tsk_i
  (if A + task_deadline tsk - task_deadline tsk_i < x
   then A + task_deadline tsk - task_deadline tsk_i
   else x) = task_request_bound_function tsk_i x rewrite ifF //.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
gtn_x: x <
A + 1 + task_deadline tsk -
task_deadline tsk_i
(A + task_deadline tsk - task_deadline tsk_i < x) =
false
        by move: gtn_x; rewrite leq_eqVlt  => /orP [/eqP EQ|LEQ]; lia. }Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
eq_x: A + 1 + task_deadline tsk - task_deadline tsk_i =
x
task_request_bound_function tsk_i
  (if A + task_deadline tsk - task_deadline tsk_i < x
   then A + task_deadline tsk - task_deadline tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i)
      {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
eq_x: A + 1 + task_deadline tsk - task_deadline tsk_i =
x
task_request_bound_function tsk_i
  (if A + task_deadline tsk - task_deadline tsk_i < x
   then A + task_deadline tsk - task_deadline tsk_i
   else x) =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i) case: (A + task_deadline tsk - task_deadline tsk_i < x).Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
eq_x: A + 1 + task_deadline tsk - task_deadline tsk_i =
x
task_request_bound_function tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i)
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
eq_x: A + 1 + task_deadline tsk - task_deadline tsk_i =
x
task_request_bound_function tsk_i x =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i)
        -Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
eq_x: A + 1 + task_deadline tsk - task_deadline tsk_i =
x
task_request_bound_function tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i) by rewrite -/rbf WL.
        -Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
ts: seq Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
D:= [eta task_deadline]: Task -> duration
rbf:= task_request_bound_function: Task -> duration -> nat
task_rbf_changes_at:= fun A : duration =>
rbf tsk A != rbf tsk (A + 1): duration -> bool
bound_on_total_hep_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  (tsk != tsko) &&
  (rbf tsko
     (A + D tsk -
      D tsko)
   != rbf tsko
        (A + 1 +
         D tsk -
         D tsko))
  in
has
  new_hep_job_released_by
  ts: duration -> bool
blocking_bound_changes_at:= fun A : duration =>
blocking_bound ts tsk
  (A - 1)
!= blocking_bound ts tsk A: duration -> bool
H_task_cost_pos: 0 < task_cost tsk
H_arrival_curve_pos: 0 < max_arrivals tsk 1
intra_IBF:= fun A F : duration =>
rbf tsk (A + 1) - task_cost tsk +
(blocking_bound ts tsk A +
 bound_on_athep_workload ts tsk A F): duration -> duration -> nat
A: nat
POSA: 0 < A
LTL: A < L
x: nat
LTx: x < L
INSP2: intra_IBF (A - 1) x <> intra_IBF A x
PI: blocking_bound ts tsk (A - 1) =
blocking_bound ts tsk A
RBF: rbf tsk A = rbf tsk (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: tsk_i != tsk
WL: rbf tsk_i
  (A + task_deadline tsk - task_deadline tsk_i) =
rbf tsk_i
  (A + 1 + task_deadline tsk -
   task_deadline tsk_i)
eq_x: A + 1 + task_deadline tsk - task_deadline tsk_i =
x
task_request_bound_function tsk_i x =
task_request_bound_function tsk_i
  (A + 1 + task_deadline tsk - task_deadline tsk_i) by rewrite eq_x. } }
  Qed.

End SearchSpaceSubset.