elf.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.elf.
Require Export prosa.analysis.facts.workload.elf_athep_bound.New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,coercions,default]
Notation "_ - _" was already used in scope
distn_scope. [notation-overridden,parsing,default]

(** * Abstract Search Space is a Subset of Restricted Supply ELF Search Space *)
Section SearchSpaceSubset.

  (** Consider any type of tasks with relative priority points. *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.
  Context `{TaskMaxNonpreemptiveSegment Task}.
  Context `{PriorityPoint 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.

  (** Consider any FP policy. *)
  Context {FP : FP_policy Task}.

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

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

  (** To reduce the time complexity of the analysis, we introduce the
      notion of a search space for ELF. 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 ELF, we consider three
      conditions.

      First, we ask whether [rbf A ≠ rbf (A + ε)]. *)
  Let task_rbf_changes_at (A : duration) :=
    task_rbf A != task_rbf (A + ε).

  (** Second, we limit our search space to those arrival offsets where
      the bound on higher-or-equal priority workload changes in value.

      Since the bound on workload from higher priority task does not depend
      on the arrival offset [A], we are only concerned about the workload from
      equal priority tasks.
      For this, we ask whether there exists a task [tsko ≠ tsk] in task set [ts]
      such that
     [ep_task_interfering_interval_length tsk tsko (A - ε) != ep_task_interfering_interval_length tsk tsko A]. *)
  Let bound_on_ep_task_workload_changes_at (A : duration) :=
    let new_hep_job_released_by tsko :=
      (ep_task tsk tsko) && (tsko != tsk)
      && (ep_task_interfering_interval_length tsk tsko (A - ε) != ep_task_interfering_interval_length tsk tsko A)
    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 ELF is the set of offsets less
      than [L] and where [task_rbf], [blocking_bound] or
      [bound_on_ep_task_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_ep_task_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) :=
    task_rbf (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
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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_ep_task_workload_changes_at 0
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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_ep_task_workload_changes_at A
    {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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_ep_task_workload_changes_at 0 apply/orP; left; apply/orP; right.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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 /task_rbf task_rbf_0_zero //=.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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 (0 + 1)
      {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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 (0 + 1) rewrite eq_sym -lt0n add0n.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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_ep_task_workload_changes_at A
    {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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_ep_task_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
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_ep_task_workload_changes_at A
false
      exfalso; apply INSP2.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_ep_task_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
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_ep_task_workload_changes_at A
task_rbf (A + 1) - task_cost tsk +
(blocking_bound ts tsk (A - 1) +
 bound_on_athep_workload ts tsk (A - 1) x) =
task_rbf (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
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_ep_task_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 /bound_on_ep_task_workload /bound_on_hp_task_workload /ep_task_interfering_interval_length.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_ep_task_workload_changes_at A
total_hp_request_bound_function_FP ts tsk x +
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
                    (tsk_o != tsk))
   task_request_bound_function tsk_o
     (minn
        `|Order.Def.max 0%R
            ((A - 1 + 1)%:R + task_priority_point tsk -
             task_priority_point tsk_o)%R| x) ==
total_hp_request_bound_function_FP ts tsk x +
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
                    (tsk_o != tsk))
   task_request_bound_function tsk_o
     (minn
        `|Order.Def.max 0%R
            ((A + 1)%:R + task_priority_point tsk -
             task_priority_point tsk_o)%R| x)
      rewrite subnK //.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_ep_task_workload_changes_at A
total_hp_request_bound_function_FP ts tsk x +
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
                    (tsk_o != tsk))
   task_request_bound_function tsk_o
     (minn
        `|Order.Def.max 0%R
            (A%:R + task_priority_point tsk -
             task_priority_point tsk_o)%R| x) ==
total_hp_request_bound_function_FP ts tsk x +
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
                    (tsk_o != tsk))
   task_request_bound_function tsk_o
     (minn
        `|Order.Def.max 0%R
            ((A + 1)%:R + task_priority_point tsk -
             task_priority_point tsk_o)%R| x)
      rewrite eqn_add2l.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_ep_task_workload_changes_at A
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
                    (tsk_o != tsk))
   task_request_bound_function tsk_o
     (minn
        `|Order.Def.max 0%R
            (A%:R + task_priority_point tsk -
             task_priority_point tsk_o)%R| x) ==
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
                    (tsk_o != tsk))
   task_request_bound_function tsk_o
     (minn
        `|Order.Def.max 0%R
            ((A + 1)%:R + task_priority_point tsk -
             task_priority_point tsk_o)%R| x)
      apply /eqP; rewrite big_seq_cond [RHS]big_seq_cond.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_ep_task_workload_changes_at A
\sum_(i <- ts | [&& i \in ts, ep_task tsk i
                  & i != tsk])
   task_request_bound_function i
     (minn
        `|Order.Def.max 0%R
            (A%:R + task_priority_point tsk -
             task_priority_point i)%R| x) =
\sum_(i <- ts | [&& i \in ts, ep_task tsk i
                  & i != tsk])
   task_request_bound_function i
     (minn
        `|Order.Def.max 0%R
            ((A + 1)%:R + task_priority_point tsk -
             task_priority_point i)%R| x)
      apply eq_big => // tsk_i /andP [TS OTHER].Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
WL: ~~ bound_on_ep_task_workload_changes_at A
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         ((A + 1)%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x)
      move: WL.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
~~ bound_on_ep_task_workload_changes_at A ->
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         ((A + 1)%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x)
      rewrite /bound_on_ep_task_workload_changes_at /ep_task_interfering_interval_length => /hasPn WL.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
WL: {in ts,
  forall x : Task,
  ~~
  (ep_task tsk x && (x != tsk) &&
   (((A - 1 + 1)%:R + task_priority_point tsk -
     task_priority_point x)%R
    != ((A + 1)%:R + task_priority_point tsk -
        task_priority_point x)%R))}
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         ((A + 1)%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x)
      move: {WL} (WL tsk_i TS) =>  /nandP [/negbTE EQ|/negPn/eqP WL].Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
EQ: ep_task tsk tsk_i && (tsk_i != tsk) = false
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         ((A + 1)%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x)
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
WL: ((A - 1 + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
         task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         ((A + 1)%:R + task_priority_point tsk -
         task_priority_point tsk_i)%R| x)
      {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
EQ: ep_task tsk tsk_i && (tsk_i != tsk) = false
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         ((A + 1)%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) by move: OTHER; rewrite EQ. }Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
WL: ((A - 1 + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         ((A + 1)%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x)
      have [leq_x|gtn_x] := leqP `|Num.max 0%R (ep_task_interfering_interval_length tsk tsk_i A)| x.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
WL: ((A - 1 + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R
leq_x: `|Order.Def.max 0%R
    (ep_task_interfering_interval_length tsk
       tsk_i A)| <= x
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  `|Order.Def.max 0%R
      (ep_task_interfering_interval_length tsk tsk_i A)|
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
WL: ((A - 1 + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R
gtn_x: x <
`|Order.Def.max 0%R
    (ep_task_interfering_interval_length tsk
       tsk_i A)|
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
         task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i x
      {Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
WL: ((A - 1 + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R
leq_x: `|Order.Def.max 0%R
    (ep_task_interfering_interval_length tsk
       tsk_i A)| <= x
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  `|Order.Def.max 0%R
      (ep_task_interfering_interval_length tsk tsk_i A)| move: WL.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
leq_x: `|Order.Def.max 0%R
    (ep_task_interfering_interval_length tsk
       tsk_i A)| <= x
((A - 1 + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R ->
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  `|Order.Def.max 0%R
      (ep_task_interfering_interval_length tsk tsk_i A)|
        rewrite subnK // /task_rbf => WL.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
leq_x: `|Order.Def.max 0%R
    (ep_task_interfering_interval_length tsk
       tsk_i A)| <= x
WL: (A%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i
  `|Order.Def.max 0%R
      (ep_task_interfering_interval_length tsk tsk_i A)|
        by rewrite WL (minn_idPl leq_x). }Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
WL: ((A - 1 + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R
gtn_x: x <
`|Order.Def.max 0%R
    (ep_task_interfering_interval_length tsk
       tsk_i A)|
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i x
      move: WL.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
gtn_x: x <
`|Order.Def.max 0%R
    (ep_task_interfering_interval_length tsk
       tsk_i A)|
((A - 1 + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R ->
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i x
      rewrite subnK // /task_rbf => WL.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
H2: PriorityPoint Task
ts: seq Task
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts
  max_arrivals
FP: FP_policy Task
tsk: Task
H_tsk_in_ts: tsk \in ts
L: duration
H_L_positive: 0 < L
task_rbf:= task_request_bound_function tsk: duration -> nat
task_rbf_changes_at:= fun A : duration =>
task_rbf A != task_rbf (A + 1): duration -> bool
bound_on_ep_task_workload_changes_at:= fun A : duration
=>
let
  new_hep_job_released_by :=
  fun tsko : Task
  =>
  ep_task tsk
    tsko &&
  (tsko != tsk) &&
  (ep_task_interfering_interval_length
     tsk tsko
     (A - 1)
   != ep_task_interfering_interval_length
        tsk tsko
        A) 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 =>
task_rbf (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: task_rbf A = task_rbf (A + 1)
tsk_i: Task
TS: tsk_i \in ts
OTHER: ep_task tsk tsk_i && (tsk_i != tsk)
gtn_x: x <
`|Order.Def.max 0%R
    (ep_task_interfering_interval_length tsk
       tsk_i A)|
WL: (A%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R =
((A + 1)%:R + task_priority_point tsk -
 task_priority_point tsk_i)%R
task_request_bound_function tsk_i
  (minn
     `|Order.Def.max 0%R
         (A%:R + task_priority_point tsk -
          task_priority_point tsk_i)%R| x) =
task_request_bound_function tsk_i x
      by rewrite WL (minn_idPr (ltnW gtn_x)). }
  Qed.

End SearchSpaceSubset.