Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.results.edf.rta.bounded_nps.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.implementation.refinements.fast_search_space_computation.[Loading ML file paramcoq.cmxs (using legacy method) ... done ]
(** First, we define the concept of higher-or-equal-priority workload. *)
Definition bound_on_total_hep_workload (ts : seq Task) (tsk : Task) A Δ :=
\sum_(tsk_o <- ts | tsk_o != tsk)
task_rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
(** Next, we provide a function that checks a single point [P=(A,F)] of the search space when
adopting a fully-preemptive policy. *)
Definition check_point_FP (ts : seq Task) (tsk : Task) (R : nat) (P : nat * nat) :=
(task_rbf tsk (P.1 + ε) + bound_on_total_hep_workload ts tsk P.1 (P.1 + P.2 ) <= P.1 + P.2 )
&& (P.2 <= R).
(** Further, we provide a way to compute the blocking bound when using nonpreemptive policies. *)
Definition blocking_bound_NP (ts : seq Task) (tsk : Task) (A : nat) :=
\max_(tsk_o <- [seq i | i <- ts] | blocking_relevant tsk_o &&
(task_deadline tsk + A <
task_deadline tsk_o)) (task_cost tsk_o - ε).
(** Finally, we provide a function that checks a single point [P=(A,F)] of the search space when
adopting a fully-nonpreemptive policy. *)
Definition check_point_NP (ts : seq Task) (tsk : Task) (R : nat) (P : nat * nat) :=
(blocking_bound_NP ts tsk P.1
+ (task_rbf tsk (P.1 + ε) - (task_cost tsk - ε))
+ bound_on_total_hep_workload ts tsk P.1 (P.1 + P.2 ) <= P.1 + P.2 )
&& (P.2 + (task_cost tsk - ε) <= R).
(** * Search Space Definitions *)
Section SearchSpaceDefinition .
(** Assume that an arrival curve based on a concrete prefix is given. *)
#[local] Existing Instance ConcreteMaxArrivals .
Definition Task := concrete_task : eqType.
Definition Job := concrete_job : eqType.
Context (TMNSP : TaskMaxNonpreemptiveSegment Task).
(** First, we recall the notion of correct search space as defined by
abstract RTA. *)
Definition correct_search_space ts (tsk :Task) L :=
[seq A <- iota 0 L | is_in_search_space ts tsk L A].
(** Next, we provide a computation-oriented way to compute abstract RTA's search space for
fixed-priority schedules, as we will prove that earliest-deadline-first is equivalent.
We start with a function that computes the search space in a generic
interval <<[l,r)>>, ... *)
Definition search_space_emax_FP_h (tsk : Task) l r :=
let h := get_horizon_of_task tsk in
let offsets := map (muln h) (iota l r) in
let emax_offsets := repeat_steps_with_offset tsk offsets in
map predn emax_offsets.
(** ... which we then apply to the interval <<[0, (L %/h).+1)>>. *)
Definition search_space_emax_FP L (tsk : Task) :=
let h := get_horizon_of_task tsk in
search_space_emax_FP_h (tsk : Task) 0 (L %/h).+1 .
(** Analogously, we define the search space for a task scheduled under earliest-deadline-first
in a generic interval <<[l,r)>>, ... *)
Definition task_search_space_emax_EDF_h (tsk tsko : Task) (l r : nat) :=
let h := get_horizon_of_task tsko in
let offsets := map (muln h) (iota l r) in
let emax_offsets := repeat_steps_with_offset tsko offsets in
let emax_edf_offsets := shift_points_neg (shift_points_pos emax_offsets (task_deadline tsko))
(task_deadline tsk) in
map predn emax_edf_offsets.
(** ...which we then apply to the interval <<[0, (L %/h).+1)>>. *)
Definition task_search_space_emax_EDF (tsk tsko : Task) (L : nat) :=
let h := get_horizon_of_task tsko in
task_search_space_emax_EDF_h tsk tsko
0 ((L + (task_deadline tsk - task_deadline tsko)) %/ h).+1 .
(** Finally, we define the overall search space as the concatenation of per-task search
spaces. *)
Definition search_space_emax_EDF ts (tsk : Task) (L : nat) :=
\cat_(tsko <- ts) task_search_space_emax_EDF tsk tsko L.
End SearchSpaceDefinition .
(** * Fast Search Space Computation Lemmas *)
Section FastSearchSpaceComputationSubset .
(** Consider a given maximum busy-interval length [L], ... *)
Variable L : duration.
(** ... a task set [ts] with valid arrivals, positive task costs, and arrival curves
with positive steps, ... *)
Variable ts : seq Task.
Hypothesis H_valid_task_set : task_set_with_valid_arrivals ts.
Hypothesis H_all_tsk_positive_cost : forall tsk , tsk \in ts -> 0 < task_cost tsk.
Hypothesis H_all_tsk_positive_step :
forall tsk , tsk \in ts -> fst (head (0 ,0 ) (steps_of (get_arrival_curve_prefix tsk))) > 0 .
(** ... and a task belonging to [ts]. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** First, we show that the earliest-deadline-first search space is a generalization of
the fixed-priority search space. *)
Lemma EDF_ss_generalize_FP_ss :
task_search_space_emax_EDF_h
tsk tsk 0 ((L + (task_deadline tsk - task_deadline tsk)) %/ get_horizon_of_task tsk).+1
= search_space_emax_FP L tsk.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts
task_search_space_emax_EDF_h tsk tsk 0
((L + (task_deadline tsk - task_deadline tsk))
%/ get_horizon_of_task tsk).+1 =
search_space_emax_FP L tsk
Proof .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts
task_search_space_emax_EDF_h tsk tsk 0
((L + (task_deadline tsk - task_deadline tsk))
%/ get_horizon_of_task tsk).+1 =
search_space_emax_FP L tsk
rewrite /task_search_space_emax_EDF_h /search_space_emax_FP /search_space_emax_FP_h.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts
[seq i.-1
| i <- shift_points_neg
(shift_points_pos
(repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsk))
%/ get_horizon_of_task
tsk).+1 ])
(task_deadline tsk))
(task_deadline tsk)] =
[seq i.-1
| i <- repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
(L %/ get_horizon_of_task tsk).+1 ]]
rewrite subnn addn0.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts
[seq i.-1
| i <- shift_points_neg
(shift_points_pos
(repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
(L
%/ get_horizon_of_task
tsk).+1 ])
(task_deadline tsk))
(task_deadline tsk)] =
[seq i.-1
| i <- repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
(L %/ get_horizon_of_task tsk).+1 ]]
set (S := repeat_steps_with_offset _ _) in *.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts S := repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
(L %/ get_horizon_of_task tsk).+1 ] : seq nat
[seq i.-1
| i <- shift_points_neg
(shift_points_pos S (task_deadline tsk))
(task_deadline tsk)] = [seq i.-1 | i <- S]
replace (shift_points_neg _ _) with S; first by done .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts S := repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
(L %/ get_horizon_of_task tsk).+1 ] : seq nat
S =
shift_points_neg
(shift_points_pos S (task_deadline tsk))
(task_deadline tsk)
symmetry ; unfold shift_points_neg, shift_points_pos.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts S := repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
(L %/ get_horizon_of_task tsk).+1 ] : seq nat
[seq x - task_deadline tsk
| x <- [seq task_deadline tsk + i | i <- S]
& task_deadline tsk <= x] = S
elim : S => [//|a S IHS].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts a : nat S : seq nat IHS : [seq x - task_deadline tsk
| x <- [seq task_deadline tsk + i | i <- S]
& task_deadline tsk <= x] = S
[seq x - task_deadline tsk
| x <- [seq task_deadline tsk + i | i <- a :: S]
& task_deadline tsk <= x] = a :: S
rewrite //= leq_addr //= IHS.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts a : nat S : seq nat IHS : [seq x - task_deadline tsk
| x <- [seq task_deadline tsk + i | i <- S]
& task_deadline tsk <= x] = S
task_deadline tsk + a - task_deadline tsk :: S =
a :: S
by replace ( _ + _ - _) with a; last lia .
Qed .
(** Finally, we show that the abstract RTA's standard search space is a subset of the
computation-oriented version defined above. *)
Lemma search_space_subset_EDF :
forall A , A \in correct_search_space ts tsk L -> A \in search_space_emax_EDF ts tsk L.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts
forall A : Datatypes_nat__canonical__eqtype_Equality,
A \in correct_search_space ts tsk L ->
A \in search_space_emax_EDF ts tsk L
Proof .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts
forall A : Datatypes_nat__canonical__eqtype_Equality,
A \in correct_search_space ts tsk L ->
A \in search_space_emax_EDF ts tsk L
move => A; unfold correct_search_space, is_in_search_space.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality
A
\in [seq A <- iota 0 L
| A < L
& task_rbf_changes_at tsk A
|| bound_on_total_hep_workload_changes_at
ts tsk A] ->
A \in search_space_emax_EDF ts tsk L
rewrite mem_filter => /andP [/andP [LT /orP [CH|CH]] IN]; unfold search_space_emax_EDF.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality LT : A < L CH : task_rbf_changes_at tsk A IN : A \in iota 0 L
A
\in \cat_(tsko<-ts)
task_search_space_emax_EDF tsk tsko L
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality LT : A < L CH : task_rbf_changes_at tsk A IN : A \in iota 0 L
A
\in \cat_(tsko<-ts)
task_search_space_emax_EDF tsk tsko L
move : (H_tsk_in_ts) => INTS.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality LT : A < L CH : task_rbf_changes_at tsk A IN : A \in iota 0 L INTS : tsk \in ts
A
\in \cat_(tsko<-ts)
task_search_space_emax_EDF tsk tsko L
apply in_cat in INTS; destruct INTS as [ts_l [ts_r EQ]].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality LT : A < L CH : task_rbf_changes_at tsk A IN : A \in iota 0 L ts_l, ts_r : seq Task EQ : ts = ts_l ++ [:: tsk] ++ ts_r
A
\in \cat_(tsko<-ts)
task_search_space_emax_EDF tsk tsko L
rewrite EQ; rewrite big_cat big_cons //= !mem_cat; apply /orP; right ; apply /orP; left .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality LT : A < L CH : task_rbf_changes_at tsk A IN : A \in iota 0 L ts_l, ts_r : seq Task EQ : ts = ts_l ++ [:: tsk] ++ ts_r
A \in task_search_space_emax_EDF tsk tsk L
unfold task_search_space_emax_EDF; rewrite EDF_ss_generalize_FP_ss.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality LT : A < L CH : task_rbf_changes_at tsk A IN : A \in iota 0 L ts_l, ts_r : seq Task EQ : ts = ts_l ++ [:: tsk] ++ ts_r
A \in search_space_emax_FP L tsk
by eapply task_search_space_subset; eauto . } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality LT : A < L CH : bound_on_total_hep_workload_changes_at ts tsk A IN : A \in iota 0 L
A
\in \cat_(tsko<-ts)
task_search_space_emax_EDF tsk tsko L
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality LT : A < L CH : bound_on_total_hep_workload_changes_at ts tsk A IN : A \in iota 0 L
A
\in \cat_(tsko<-ts)
task_search_space_emax_EDF tsk tsko L
move : CH => /hasP [tsko INts /andP [NEQtsk NEQ]].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts H_all_tsk_positive_cost : forall tsk : Task,
tsk \in ts ->
0 < task_cost tskH_all_tsk_positive_step : forall tsk : Task,
tsk \in ts ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 tsk : Task H_tsk_in_ts : tsk \in ts A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L tsko : Task INts : tsko \in ts NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko)
A
\in \cat_(tsko<-ts)
task_search_space_emax_EDF tsk tsko L
apply in_cat in INts; destruct INts as [ts_l [ts_r EQ]]; subst .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko)
A
\in \cat_(tsko<-(ts_l ++ [:: tsko] ++ ts_r))
task_search_space_emax_EDF tsk tsko L
have INts:tsko \in ts_l++[::tsko]++ts_r by rewrite !mem_cat mem_seq1; apply /orP;right ;apply /orP;left .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r
A
\in \cat_(tsko<-(ts_l ++ [:: tsko] ++ ts_r))
task_search_space_emax_EDF tsk tsko L
rewrite big_cat big_cons //= !mem_cat; apply /orP; right ; apply /orP; left ; apply /mapP.L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r
exists2 x : Datatypes_nat__canonical__eqtype_Equality,
x
\in shift_points_neg
(shift_points_pos
(repeat_steps_with_offset tsko
[seq get_horizon_of_task tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ get_horizon_of_task
tsko).+1 ])
(task_deadline tsko)) (task_deadline tsk) &
A = x.-1
exists A .+1 ; last by lia .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r
A.+1
\in shift_points_neg
(shift_points_pos
(repeat_steps_with_offset tsko
[seq get_horizon_of_task tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ get_horizon_of_task tsko).+1 ])
(task_deadline tsko)) (task_deadline tsk)
apply /mapP; exists (A .+1 + task_deadline tsk); last by rewrite -addnBA // subnn addn0.L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r
A.+1 + task_deadline tsk
\in [seq x <- shift_points_pos
(repeat_steps_with_offset tsko
[seq get_horizon_of_task tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ get_horizon_of_task
tsko).+1 ])
(task_deadline tsko)
| task_deadline tsk <= x]
rewrite mem_filter; apply /andP; split ; first by lia .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r
A.+1 + task_deadline tsk
\in shift_points_pos
(repeat_steps_with_offset tsko
[seq get_horizon_of_task tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ get_horizon_of_task tsko).+1 ])
(task_deadline tsko)
have AD : task_deadline tsko <= A + task_deadline tsk.L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r
task_deadline tsko <= A + task_deadline tsk
{ L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r
task_deadline tsko <= A + task_deadline tsk
move_neq_up CONTR. L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r CONTR : A + task_deadline tsk < task_deadline tsko
False
have Z1 : A + task_deadline tsk - task_deadline tsko = 0 by lia .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r CONTR : A + task_deadline tsk < task_deadline tsko Z1 : A + task_deadline tsk - task_deadline tsko = 0
False
have Z2 : A + 1 + task_deadline tsk - task_deadline tsko = 0 by lia .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r CONTR : A + task_deadline tsk < task_deadline tsko Z1 : A + task_deadline tsk - task_deadline tsko = 0 Z2 : A + 1 + task_deadline tsk - task_deadline tsko =
0
False
by rewrite Z1 Z2 eq_refl in NEQ. } L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk
A.+1 + task_deadline tsk
\in shift_points_pos
(repeat_steps_with_offset tsko
[seq get_horizon_of_task tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ get_horizon_of_task tsko).+1 ])
(task_deadline tsko)
apply /mapP; exists (A .+1 + task_deadline tsk - task_deadline tsko); last by rewrite subnKC; lia .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk
A.+1 + task_deadline tsk - task_deadline tsko
\in repeat_steps_with_offset tsko
[seq get_horizon_of_task tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ get_horizon_of_task tsko).+1 ]
set rto := repeat_steps_with_offset; set ght := get_horizon_of_task.L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration
A.+1 + task_deadline tsk - task_deadline tsko
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
have IN_RTO : forall B L' , (B \in search_space_emax_FP L' tsko) ->
B.+1 \in rto tsko [seq ght tsko * i | i <- iota 0 (L' %/ ght tsko).+1 ].L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration
forall (B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]
{ L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration
forall (B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]
move => B L' /mapP [C INC EQC].L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration B : Datatypes_nat__canonical__eqtype_Equality L' : nat C : Datatypes_nat__canonical__eqtype_Equality INC : C
\in repeat_steps_with_offset tsko
[seq get_horizon_of_task tsko * i
| i <- iota 0
(L'
%/ get_horizon_of_task tsko).+1 ] EQC : B = C.-1
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]
have POS : C > 0 by eapply nonshifted_offsets_are_positive; eauto 2 .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration B : Datatypes_nat__canonical__eqtype_Equality L' : nat C : Datatypes_nat__canonical__eqtype_Equality INC : C
\in repeat_steps_with_offset tsko
[seq get_horizon_of_task tsko * i
| i <- iota 0
(L'
%/ get_horizon_of_task tsko).+1 ] EQC : B = C.-1 POS : 0 < C
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]
by rewrite EQC prednK. } L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]
A.+1 + task_deadline tsk - task_deadline tsko
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
destruct (leqP (task_deadline tsko) (task_deadline tsk)) as [EE|EE].L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsko <= task_deadline tsk
A.+1 + task_deadline tsk - task_deadline tsko
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
{ L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsko <= task_deadline tsk
A.+1 + task_deadline tsk - task_deadline tsko
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
rewrite -addnBA //; rewrite -!addnBA // -addnA[1 +_] addnC addnA in NEQ.L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsko <= task_deadline tsk NEQ : task_request_bound_function tsko
(A +
(concept.task_deadline tsk -
concept.task_deadline tsko))
!= task_request_bound_function tsko
(A +
(concept.task_deadline tsk -
concept.task_deadline tsko) + 1 )
A.+1 + (task_deadline tsk - task_deadline tsko)
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
rewrite -addn1 -addnA [1 + _ ]addnC addnA addn1.L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsko <= task_deadline tsk NEQ : task_request_bound_function tsko
(A +
(concept.task_deadline tsk -
concept.task_deadline tsko))
!= task_request_bound_function tsko
(A +
(concept.task_deadline tsk -
concept.task_deadline tsko) + 1 )
(A + (task_deadline tsk - task_deadline tsko)).+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
set (B := A + (task_deadline tsk - task_deadline tsko)) in *.L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsko <= task_deadline tsk NEQ : task_request_bound_function tsko
(A +
(concept.task_deadline tsk -
concept.task_deadline tsko))
!= task_request_bound_function tsko
(A +
(concept.task_deadline tsk -
concept.task_deadline tsko) + 1 ) B := A + (task_deadline tsk - task_deadline tsko) : nat
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
have CH : task_rbf_changes_at tsko B; [ done | clear NEQ ].L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsko <= task_deadline tsk B := A + (task_deadline tsk - task_deadline tsko) : nat CH : task_rbf_changes_at tsko B
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
have LTB : B < L + (task_deadline tsk - task_deadline tsko) by unfold B; lia .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsko <= task_deadline tsk B := A + (task_deadline tsk - task_deadline tsko) : nat CH : task_rbf_changes_at tsko B LTB : B < L + (task_deadline tsk - task_deadline tsko)
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
by apply IN_RTO; last by eapply task_search_space_subset; eauto . } L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsk < task_deadline tsko
A.+1 + task_deadline tsk - task_deadline tsko
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
{ L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsk < task_deadline tsko
A.+1 + task_deadline tsk - task_deadline tsko
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
apply ltnW in EE.L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko NEQ : task_request_bound_function tsko
(A + concept.task_deadline tsk -
concept.task_deadline tsko)
!= task_request_bound_function tsko
(A + 1 + concept.task_deadline tsk -
concept.task_deadline tsko) INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsk <= task_deadline tsko
A.+1 + task_deadline tsk - task_deadline tsko
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
rewrite -subnBA//-subnBA//-addnBAC in NEQ; last by rewrite /concept.task_deadline /TaskDeadline; lia .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsk <= task_deadline tsko NEQ : task_request_bound_function tsko
(A -
(concept.task_deadline tsko -
concept.task_deadline tsk))
!= task_request_bound_function tsko
(A -
(concept.task_deadline tsko -
concept.task_deadline tsk) + 1 )
A.+1 + task_deadline tsk - task_deadline tsko
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
rewrite -subnBA // -addn1 -addnBAC //; last by lia .L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsk <= task_deadline tsko NEQ : task_request_bound_function tsko
(A -
(concept.task_deadline tsko -
concept.task_deadline tsk))
!= task_request_bound_function tsko
(A -
(concept.task_deadline tsko -
concept.task_deadline tsk) + 1 )
A - (task_deadline tsko - task_deadline tsk) + 1
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
set (B := A - (task_deadline tsko - task_deadline tsk)) in *.L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsk <= task_deadline tsko NEQ : task_request_bound_function tsko
(A -
(concept.task_deadline tsko -
concept.task_deadline tsk))
!= task_request_bound_function tsko
(A -
(concept.task_deadline tsko -
concept.task_deadline tsk) + 1 ) B := A - (task_deadline tsko - task_deadline tsk) : nat
B + 1
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
have CH : task_rbf_changes_at tsko B; [ done | clear NEQ ].L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsk <= task_deadline tsko B := A - (task_deadline tsko - task_deadline tsk) : nat CH : task_rbf_changes_at tsko B
B + 1
\in rto tsko
[seq ght tsko * i
| i <- iota 0
((L +
(task_deadline tsk -
task_deadline tsko))
%/ ght tsko).+1 ]
replace (task_deadline tsk - task_deadline tsko) with 0 ; [rewrite addn0 addn1 |lia ].L : duration tsko : Task ts_l, ts_r : seq Task H_all_tsk_positive_step : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix
tsk))).1 H_all_tsk_positive_cost : forall tsk : Task,
tsk
\in ts_l ++
[:: tsko] ++ ts_r ->
0 < task_cost tskH_valid_task_set : task_set_with_valid_arrivals
(ts_l ++ [:: tsko] ++ ts_r) tsk : Task H_tsk_in_ts : tsk \in ts_l ++ [:: tsko] ++ ts_r A : Datatypes_nat__canonical__eqtype_Equality LT : A < L IN : A \in iota 0 L NEQtsk : tsk != tsko INts : tsko \in ts_l ++ [:: tsko] ++ ts_r AD : task_deadline tsko <= A + task_deadline tsk rto := repeat_steps_with_offset : task.Task -> seq nat -> seq nat ght := get_horizon_of_task : task.Task -> duration IN_RTO : forall
(B : Datatypes_nat__canonical__eqtype_Equality)
(L' : nat),
B \in search_space_emax_FP L' tsko ->
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L' %/ ght tsko).+1 ]EE : task_deadline tsk <= task_deadline tsko B := A - (task_deadline tsko - task_deadline tsk) : nat CH : task_rbf_changes_at tsko B
B.+1
\in rto tsko
[seq ght tsko * i
| i <- iota 0 (L %/ ght tsko).+1 ]
by apply IN_RTO; last eapply task_search_space_subset; eauto 2 ; unfold B; lia . } }
Qed .
End FastSearchSpaceComputationSubset .