Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
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]
Serlib plugin: coq-paramcoq.plugin is not available: serlib support is missing. Incremental checking for commands in this plugin will be impacted.
[Loading ML file paramcoq.cmxs (using legacy method) ... done]
Notations "[ coqeal _ of _ ]" defined at level 0 and "[ TASK id: _ cost: _ deadline: _ arrival: _ priority: _ ]" defined at level 6 have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,parsing,default]
Notations "[ coqeal _ of _ ]" defined at level 0 and "[ PERIODIC-TASK id: _ cost: _ deadline: _ period: _ priority: _ ]" defined at level 6 have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,parsing,default]
Notations "[ coqeal _ of _ ]" defined at level 0 and "[ SPORADIC-TASK id: _ cost: _ deadline: _ separation: _ priority: _ ]" defined at level 6 have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,parsing,default]
Notations "[ coqeal _ of _ ]" defined at level 0 and "[ CURVE horizon: _ steps: _ ]" defined at level 6 have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,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]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
(** In this section, we provide definitions and lemmas to show Abstract RTA' s search space can be rewritten in an equivalent, computation-oriented way. *) Section FastSearchSpaceComputation. (** Let L be a constant which bounds any busy interval of task [tsk]. *) Variable L : duration. (** Consider a task set [ts] with valid arrivals... *) Variable ts : seq Task. Hypothesis H_valid_task_set : task_set_with_valid_arrivals ts. (** ... and a task [tsk] of [ts] with positive cost. *) Variable tsk : Task. Hypothesis H_positive_cost : 0 < task_cost tsk. Hypothesis H_tsk_in_ts : tsk \in ts. Section Definitions. (** We generically define the search space for fixed-priority tasks in the interval <<[l,r)>> by repeating the time steps of the task in the interval <<[l*h,r*h)>>. *) Definition search_space_arrival_curve_prefix_FP_h (tsk : Task) l r := let h := get_horizon_of_task tsk in let offsets := map (muln h) (iota l r) in let arrival_curve_prefix_offsets := repeat_steps_with_offset tsk offsets in map predn arrival_curve_prefix_offsets. (** By using the above definition, we give a concrete definition of the search space for fixed-priority tasks. *) Definition search_space_arrival_curve_prefix_FP (tsk : Task) L := let h := get_horizon_of_task tsk in search_space_arrival_curve_prefix_FP_h (tsk : Task) 0 (L %/h).+1. End Definitions. Section Facts. (** We begin by showing that either each time step of an arrival curve prefix is either strictly less than the horizon, or it is the horizon. *)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

(forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/ last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

(forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/ last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

has_valid_arrival_curve_prefix tsk -> (forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/ last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix

(forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/ last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk

(forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/ last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
LT1: get_horizon_of_task tsk < last0 (get_time_steps_of_task tsk)
(forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/ last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk

(forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/ last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk

forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk
step: Datatypes_nat__canonical__eqtype_Equality
IN: step \in get_time_steps_of_task tsk

step < get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk
step: Datatypes_nat__canonical__eqtype_Equality
IN: step \in get_time_steps_of_task tsk

step <= last0 (get_time_steps_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk
step: Datatypes_nat__canonical__eqtype_Equality
IN: step \in get_time_steps_of_task tsk

sorted ltn (get_time_steps_of_task tsk) -> step <= last0 (get_time_steps_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk
step: Datatypes_nat__canonical__eqtype_Equality
IN: step \in get_time_steps_of_task tsk
TS_UNIQ: uniq (get_time_steps_of_task tsk)
TS_SORT: sorted leq (get_time_steps_of_task tsk)

step <= last0 (get_time_steps_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk
step: Datatypes_nat__canonical__eqtype_Equality
IN: step \in get_time_steps_of_task tsk
TS_UNIQ: uniq (get_time_steps_of_task tsk)
TS_SORT: sorted leq (get_time_steps_of_task tsk)

last0 (get_time_steps_of_task tsk) \in get_time_steps_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk
step: Datatypes_nat__canonical__eqtype_Equality
IN: step \in get_time_steps_of_task tsk
TS_UNIQ: uniq (get_time_steps_of_task tsk)
TS_SORT: sorted leq (get_time_steps_of_task tsk)
index step (get_time_steps_of_task tsk) <= index (last0 (get_time_steps_of_task tsk)) (get_time_steps_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk
step: Datatypes_nat__canonical__eqtype_Equality
IN: step \in get_time_steps_of_task tsk
TS_UNIQ: uniq (get_time_steps_of_task tsk)
TS_SORT: sorted leq (get_time_steps_of_task tsk)

last0 (get_time_steps_of_task tsk) \in get_time_steps_of_task tsk
by destruct get_time_steps_of_task; last by rewrite /last0 //=; apply mem_last.
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
GT1: last0 (get_time_steps_of_task tsk) < get_horizon_of_task tsk
step: Datatypes_nat__canonical__eqtype_Equality
IN: step \in get_time_steps_of_task tsk
TS_UNIQ: uniq (get_time_steps_of_task tsk)
TS_SORT: sorted leq (get_time_steps_of_task tsk)

index step (get_time_steps_of_task tsk) <= index (last0 (get_time_steps_of_task tsk)) (get_time_steps_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
d: duration
l: seq duration
GT1: last0 (d :: l) < get_horizon_of_task tsk
step: Datatypes_nat__canonical__eqtype_Equality
TS_UNIQ: uniq (d :: l)
TS_SORT: sorted leq (d :: l)
IN: index step (d :: l) < size (d :: l)

index step (d :: l) <= index (last0 (d :: l)) (d :: l)
by rewrite /last0; simpl (last 0 _); rewrite index_last.
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
LT1: get_horizon_of_task tsk < last0 (get_time_steps_of_task tsk)

(forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/ last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
LT1: get_horizon_of_task tsk < last0 (get_time_steps_of_task tsk)

(forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/ last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
LT1: get_horizon_of_task tsk < last0 (get_time_steps_of_task tsk)

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
d: duration
l: seq duration
TS: get_time_steps_of_task tsk = d :: l
LT1: get_horizon_of_task tsk < last0 (d :: l)

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: large_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
d: duration
l: seq duration
TS: get_time_steps_of_task tsk = d :: l
LT1: get_horizon_of_task tsk < last0 (d :: l)
IN: last0 (d :: l) \in d :: l

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
LARGEh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in time_steps_of arrival_curve_prefix -> s <= horizon_of arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
d: duration
l: seq duration
TS: time_steps_of (get_arrival_curve_prefix tsk) = d :: l
LT1: get_horizon_of_task tsk < last0 (d :: l)
IN: last0 (d :: l) \in d :: l

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
d: duration
l: seq duration
LT1: get_horizon_of_task tsk < last0 (d :: l)
IN: last0 (d :: l) \in d :: l
TS: time_steps_of arrival_curve_prefix = d :: l
LARGEh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in d :: l -> s <= horizon_of arrival_curve_prefix

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
arrival_curve_prefix: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = arrival_curve_prefix
POSh: positive_horizon arrival_curve_prefix
NOINF: no_inf_arrivals arrival_curve_prefix
BUR: specified_bursts arrival_curve_prefix
SORT: sorted_ltn_steps arrival_curve_prefix
d: duration
l: seq duration
LT1: get_horizon_of_task tsk < last0 (d :: l)
IN: last0 (d :: l) <= horizon_of arrival_curve_prefix
TS: time_steps_of arrival_curve_prefix = d :: l
LARGEh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in d :: l -> s <= horizon_of arrival_curve_prefix

False
by rewrite /get_horizon_of_task EQ in LT1; lia. } Qed. (** Next, we show that for each offset [A] in the search space for fixed-priority tasks, either (1) [A+ε] is zero or a multiple of the horizon, offset by one of the time steps of the arrival curve prefix, or (2) [A+ε] is exactly a multiple of the horizon. *)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall A : nat, A < L -> task_rbf tsk A != task_rbf tsk (A + 1) -> (exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ get_horizon_of_task tsk).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * get_horizon_of_task tsk + t) \/ (exists i : nat, i < (L %/ get_horizon_of_task tsk).+1 /\ A + 1 = i * get_horizon_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall A : nat, A < L -> task_rbf tsk A != task_rbf tsk (A + 1) -> (exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ get_horizon_of_task tsk).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * get_horizon_of_task tsk + t) \/ (exists i : nat, i < (L %/ get_horizon_of_task tsk).+1 /\ A + 1 = i * get_horizon_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

has_valid_arrival_curve_prefix tsk -> forall A : nat, A < L -> task_rbf tsk A != task_rbf tsk (A + 1) -> (exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ get_horizon_of_task tsk).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * get_horizon_of_task tsk + t) \/ (exists i : nat, i < (L %/ get_horizon_of_task tsk).+1 /\ A + 1 = i * get_horizon_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: task_rbf tsk A != task_rbf tsk (A + 1)

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ get_horizon_of_task tsk).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * get_horizon_of_task tsk + t) \/ (exists i : nat, i < (L %/ get_horizon_of_task tsk).+1 /\ A + 1 = i * get_horizon_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ get_horizon_of_task tsk).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * get_horizon_of_task tsk + t) \/ (exists i : nat, i < (L %/ get_horizon_of_task tsk).+1 /\ A + 1 = i * get_horizon_of_task tsk)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ horizon_of evec).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * horizon_of evec + t) \/ (exists i : nat, i < (L %/ horizon_of evec).+1 /\ A + 1 = i * horizon_of evec)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ horizon_of evec).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * horizon_of evec + t) \/ (exists i : nat, i < (L %/ horizon_of evec).+1 /\ A + 1 = i * horizon_of evec)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ h).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * h + t) \/ (exists i : nat, i < (L %/ h).+1 /\ A + 1 = i * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
LT: A %/ horizon_of evec < (A + 1) %/ horizon_of evec

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ h).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * h + t) \/ (exists i : nat, i < (L %/ h).+1 /\ A + 1 = i * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ h).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * h + t) \/ (exists i : nat, i < (L %/ h).+1 /\ A + 1 = i * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
LT: A %/ horizon_of evec < (A + 1) %/ horizon_of evec

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ h).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * h + t) \/ (exists i : nat, i < (L %/ h).+1 /\ A + 1 = i * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
LT: A %/ horizon_of evec < (A + 1) %/ horizon_of evec

exists i : nat, i < (L %/ h).+1 /\ A + 1 = i * h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
LT: A %/ horizon_of evec < (A + 1) %/ horizon_of evec

A + 1 = (A + 1) %/ h * h
by symmetry; apply /eqP; rewrite -dvdn_eq; by apply ltdivn_dvdn.
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ h).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * h + t) \/ (exists i : nat, i < (L %/ h).+1 /\ A + 1 = i * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ h).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * h + t) \/ (exists i : nat, i < (L %/ h).+1 /\ A + 1 = i * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ h).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * h + t
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

(A + 1) %/ h < (L %/ h).+1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
(step_at evec ((A + 1) %% h)).1 \in get_time_steps_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

(A + 1) %/ h < (L %/ h).+1
by rewrite addn1 ltnS; apply leq_div2r.
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

(step_at evec ((A + 1) %% h)).1 \in get_time_steps_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

(step_at evec ((A + 1) %% h)).1 \in get_time_steps_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

(step_at evec ((A + 1) %% h)).1 \in time_steps_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

last (0, 0) [seq s <- steps_of evec | s.1 <= (A + 1) %% h] \in steps_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
EQeps: (A + 1) %% h = A %% h + 1

last (0, 0) [seq s <- steps_of evec | s.1 <= (A + 1) %% h] \in steps_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
EQeps: (A + 1) %% h = A %% h + 1
LTe: value_at evec (A %% horizon_of evec) < value_at evec (A %% h + 1)

last (0, 0) [seq s <- steps_of evec | s.1 <= (A + 1) %% h] \in steps_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
EQeps: (A + 1) %% h = A %% h + 1
LTe: value_at evec (A %% horizon_of evec) < value_at evec (A %% h + 1)
v: Datatypes_nat__canonical__eqtype_Equality
IN: (A %% horizon_of evec + 1, v) \in steps_of evec

last (0, 0) [seq s <- steps_of evec | s.1 <= (A + 1) %% h] \in steps_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
EQeps: (A + 1) %% h = A %% h + 1
LTe: value_at evec (A %% horizon_of evec) < value_at evec (A %% h + 1)
v: Datatypes_nat__canonical__eqtype_Equality
IN: ((A + 1) %% h, v) \in steps_of evec

exists2 x : Datatypes_prod__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality, x \in steps_of evec & x.1 <= (A + 1) %% h
by exists ((A+ε) %% h, v).
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
EQs: A %/ horizon_of evec < (A + 1) %/ horizon_of evec

A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
EQs: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LT: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
EQs: A %/ horizon_of evec < (A + 1) %/ horizon_of evec

A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
k: nat
EQs: A + 1 = k * horizon_of evec

k * horizon_of evec = (k * horizon_of evec) %/ h * h + (step_at evec ((k * horizon_of evec) %% h)).1
by rewrite modnMl step_at_0_is_00; [rewrite addn0 mulnK | apply SORT |].
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
EQs: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LT: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LTe: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)
EQs: A %/ horizon_of evec = (A + 1) %/ horizon_of evec
LT: value_at evec (A %% horizon_of evec) < value_at evec ((A + 1) %% horizon_of evec)

A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ h = (A + 1) %/ h
LTe: value_at evec (A %% h) < value_at evec ((A + 1) %% h)
EQs: A %/ h = (A + 1) %/ h
LT: value_at evec (A %% h) < value_at evec ((A + 1) %% h)

A + 1 = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ h = (A + 1) %/ h
LTe: value_at evec (A %% h) < value_at evec ((A + 1) %% h)
EQs: A %/ h = (A + 1) %/ h
LT: value_at evec (A %% h) < value_at evec ((A + 1) %% h)

(A + 1) %/ h * h + (A + 1) %% h = (A + 1) %/ h * h + (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ h = (A + 1) %/ h
LTe: value_at evec (A %% h) < value_at evec ((A + 1) %% h)
EQs: A %/ h = (A + 1) %/ h
LT: value_at evec (A %% h) < value_at evec ((A + 1) %% h)

(A + 1) %% h = (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ h = (A + 1) %/ h
LTe: value_at evec (A %% h) < value_at evec ((A + 1) %% h)
EQs: A %/ h = (A + 1) %/ h
LT: value_at evec (A %% h) < value_at evec (A %% h + 1 %% h)

(A + 1) %% h = (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ h = (A + 1) %/ h
LTe: value_at evec (A %% h) < value_at evec ((A + 1) %% h)
EQs: A %/ h = (A + 1) %/ h
LT: value_at evec (A %% h) < value_at evec (A %% h + 1 %% h)
EQ1: 1 %% h = 1

(A + 1) %% h = (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ h = (A + 1) %/ h
LTe: value_at evec (A %% h) < value_at evec ((A + 1) %% h)
EQs: A %/ h = (A + 1) %/ h
EQ1: 1 %% h = 1
LT: exists v : Datatypes_nat__canonical__eqtype_Equality, (A %% h + 1, v) \in steps_of evec

(A + 1) %% h = (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ h = (A + 1) %/ h
LTe: value_at evec (A %% h) < value_at evec ((A + 1) %% h)
EQs: A %/ h = (A + 1) %/ h
EQ1: 1 %% h = 1
v: Datatypes_nat__canonical__eqtype_Equality
IN: (A %% h + 1, v) \in steps_of evec

(A + 1) %% h = (step_at evec ((A + 1) %% h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ h = (A + 1) %/ h
LTe: value_at evec (A %% h) < value_at evec ((A + 1) %% h)
EQs: A %/ h = (A + 1) %/ h
EQ1: 1 %% h = 1
v: Datatypes_nat__canonical__eqtype_Equality
IN: (A %% h + 1, v) \in steps_of evec

A %% h + 1 %% h - 0 * h = (step_at evec (A %% h + 1 %% h - 0 * h)).1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EQ: get_arrival_curve_prefix tsk = evec
h:= horizon_of evec: duration
POSh: 0 < h
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT_L: A < L
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQdiv: A %/ h = (A + 1) %/ h
LTe: value_at evec (A %% h) < value_at evec ((A + 1) %% h)
EQs: A %/ h = (A + 1) %/ h
EQ1: 1 %% h = 1
v: Datatypes_nat__canonical__eqtype_Equality
IN: step_at evec (A %% h + 1) = (A %% h + 1, v)

A %% h + 1 %% h - 0 * h = (step_at evec (A %% h + 1 %% h - 0 * h)).1
by rewrite subn0 !EQ1 IN. } } } Qed. (** Conversely, every multiple of the horizon that is strictly less than [L] is contained in the search space for fixed-priority tasks... *)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall A : nat, A < L -> get_horizon_of_task tsk %| A -> A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall A : nat, A < L -> get_horizon_of_task tsk %| A -> A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
VALID: valid_arrival_curve_prefix evec

forall A : nat, A < L -> get_horizon_of_task tsk %| A -> A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
VALID: valid_arrival_curve_prefix evec
A: nat
LT: A < L
DIV: get_horizon_of_task tsk %| A

A \in search_space_arrival_curve_prefix_FP_h tsk 0 (L %/ get_horizon_of_task tsk).+1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT: A < L
DIV: get_horizon_of_task tsk %| A

A \in search_space_arrival_curve_prefix_FP_h tsk 0 (L %/ get_horizon_of_task tsk).+1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT: A < L
DIV: get_horizon_of_task tsk %| A

A + 1 - 1 \in search_space_arrival_curve_prefix_FP_h tsk 0 (L %/ get_horizon_of_task tsk).+1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT: A < L
DIV: get_horizon_of_task tsk %| A

A + 1 \in repeat_steps_with_offset tsk [seq get_horizon_of_task tsk * i | i <- iota 0 (L %/ get_horizon_of_task tsk).+1]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT: A < L
h:= get_horizon_of_task tsk: duration
DIV: h %| A

A + 1 \in repeat_steps_with_offset tsk [seq h * i | i <- iota 0 (L %/ h).+1]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LT: A < L
h:= get_horizon_of_task tsk: duration
DIV: h %| A

exists2 x : Datatypes_nat__canonical__eqtype_Equality, x \in [seq h * i | i <- iota 0 (L %/ h).+1] & A + 1 \in time_steps_with_offset tsk x
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

exists2 x : Datatypes_nat__canonical__eqtype_Equality, x \in [seq h * i | i <- iota 0 (L %/ h).+1] & k * h + 1 \in time_steps_with_offset tsk x
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

k * h \in [seq h * i | i <- iota 0 (L %/ h).+1]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L
k * h + 1 \in time_steps_with_offset tsk (k * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

k * h \in [seq h * i | i <- iota 0 (L %/ h).+1]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

k \in iota 0 (L %/ h).+1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

k < 0 + (L %/ h).+1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

0 < h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L
BUR: 1 \in time_steps_of evec

0 < h
by rewrite /h /get_horizon_of_task EMAX.
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

k * h + 1 \in time_steps_with_offset tsk (k * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

k * h + 1 \in time_steps_with_offset tsk (k * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

1 + k * h \in [seq t + k * h | t <- get_time_steps_of_task tsk]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
h:= get_horizon_of_task tsk: duration
k: nat
LT: k * h < L

1 \in get_time_steps_of_task tsk
by rewrite /get_time_steps_of_task EMAX; apply BUR. } Qed. (** ... and every [A] for which [A+ε] is a multiple of the horizon offset by a time step of the arrival curve prefix is also in the search space for fixed-priority tasks. *)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality) (A : nat), i < (L %/ get_horizon_of_task tsk).+1 -> t \in get_time_steps_of_task tsk -> A + 1 = i * get_horizon_of_task tsk + t -> A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality) (A : nat), i < (L %/ get_horizon_of_task tsk).+1 -> t \in get_time_steps_of_task tsk -> A + 1 = i * get_horizon_of_task tsk + t -> A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
VALID: task_set_with_valid_arrivals ts
i: nat
t: Datatypes_nat__canonical__eqtype_Equality
A: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
IN: t \in get_time_steps_of_task tsk
EQ: A + 1 = i * get_horizon_of_task tsk + t

A \in search_space_arrival_curve_prefix_FP_h tsk 0 (L %/ get_horizon_of_task tsk).+1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
VALID: task_set_with_valid_arrivals ts
i: nat
t: Datatypes_nat__canonical__eqtype_Equality
A: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
IN: t \in get_time_steps_of_task tsk
EQ: A + 1 = i * get_horizon_of_task tsk + t

A + 1 - 1 \in search_space_arrival_curve_prefix_FP_h tsk 0 (L %/ get_horizon_of_task tsk).+1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
VALID: task_set_with_valid_arrivals ts
i: nat
t: Datatypes_nat__canonical__eqtype_Equality
A: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
IN: t \in get_time_steps_of_task tsk
EQ: A + 1 = i * get_horizon_of_task tsk + t

A + 1 \in repeat_steps_with_offset tsk [seq get_horizon_of_task tsk * i | i <- iota 0 (L %/ get_horizon_of_task tsk).+1]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
VALID: task_set_with_valid_arrivals ts
i: nat
t: Datatypes_nat__canonical__eqtype_Equality
A: nat
h:= get_horizon_of_task tsk: duration
LT: i < (L %/ h).+1
IN: t \in get_time_steps_of_task tsk
EQ: A + 1 = i * h + t

A + 1 \in repeat_steps_with_offset tsk [seq h * i | i <- iota 0 (L %/ h).+1]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
VALID: task_set_with_valid_arrivals ts
i: nat
t: Datatypes_nat__canonical__eqtype_Equality
A: nat
h:= get_horizon_of_task tsk: duration
LT: i < (L %/ h).+1
IN: t \in get_time_steps_of_task tsk
EQ: A + 1 = i * h + t

exists2 x : Datatypes_nat__canonical__eqtype_Equality, x \in [seq h * i | i <- iota 0 (L %/ h).+1] & A + 1 \in time_steps_with_offset tsk x
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
VALID: task_set_with_valid_arrivals ts
i: nat
t: Datatypes_nat__canonical__eqtype_Equality
A: nat
h:= get_horizon_of_task tsk: duration
LT: i < (L %/ h).+1
IN: t \in get_time_steps_of_task tsk
EQ: A + 1 = i * h + t

A + 1 \in time_steps_with_offset tsk (i * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
VALID: task_set_with_valid_arrivals ts
i: nat
t: Datatypes_nat__canonical__eqtype_Equality
A: nat
h:= get_horizon_of_task tsk: duration
LT: i < (L %/ h).+1
IN: t \in get_time_steps_of_task tsk
EQ: A + 1 = i * h + t

A + 1 \in [seq t + i * h | t <- get_time_steps_of_task tsk]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
VALID: task_set_with_valid_arrivals ts
i: nat
t: Datatypes_nat__canonical__eqtype_Equality
A: nat
h:= get_horizon_of_task tsk: duration
LT: i < (L %/ h).+1
IN: t \in get_time_steps_of_task tsk
EQ: A + 1 = i * h + t

t + i * h \in [seq t + i * h | t <- get_time_steps_of_task tsk]
by apply (map_f (fun t0 => t0 + i * h) IN). Qed. (** Next, we show that if the horizon of the arrival curve prefix divides [A+ε], then [A] is not contained in the search space for fixed-priority tasks. *)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall A : nat, (forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) -> get_horizon_of_task tsk %| A + 1 -> max_arrivals tsk A = max_arrivals tsk (A + 1)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall A : nat, (forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) -> get_horizon_of_task tsk %| A + 1 -> max_arrivals tsk A = max_arrivals tsk (A + 1)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

has_valid_arrival_curve_prefix tsk -> forall A : nat, (forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) -> get_horizon_of_task tsk %| A + 1 -> max_arrivals tsk A = max_arrivals tsk (A + 1)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
DIV: get_horizon_of_task tsk %| A + 1

max_arrivals tsk A = max_arrivals tsk (A + 1)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
DIV: get_horizon_of_task tsk %| A + 1

extrapolated_arrival_curve evec A = extrapolated_arrival_curve evec (A + 1)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
DIV: horizon_of evec %| A + 1
MOD0: (A + 1) %% horizon_of evec = 0

extrapolated_arrival_curve evec A = extrapolated_arrival_curve evec (A + 1)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
DIV: horizon_of evec %| A + 1
MOD0: (A + 1) %% horizon_of evec = 0

A %/ horizon_of evec * value_at evec (horizon_of evec) + value_at evec (A %% horizon_of evec) = (A + 1) %/ horizon_of evec * value_at evec (horizon_of evec) + value_at evec ((A + 1) %% horizon_of evec)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat

A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h

A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
LT1: h < 1
A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
EQ1: 1 = h
A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h

A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

vec (A %% h) = vec h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0
A %/ h * vec h + vec h = (A + 1) %/ h * vec h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

vec (A %% h) = vec h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

(step_at evec (A %% h)).2 = (step_at evec h).2
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

step_at evec (A %% h) = step_at evec h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

step_at evec (if h %| A + 1 then h.-1 else ((A + 1) %% h).-1) = step_at evec h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

last (0, 0) [seq step <- steps_of evec | step.1 <= h.-1] = last (0, 0) [seq step <- steps_of evec | step.1 <= h]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

[seq step <- steps_of evec | step.1 <= h] = steps_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0
last (0, 0) [seq step <- steps_of evec | step.1 <= h.-1] = last (0, 0) (steps_of evec)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

[seq step <- steps_of evec | step.1 <= h] = steps_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
DIV: horizon_of evec %| A + 1
MOD0: (A + 1) %% horizon_of evec = 0
vec:= value_at evec: duration -> nat
GT1: 1 < horizon_of evec
NOINF: value_at evec 0 = 0
step: Datatypes_prod__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality
IN: step \in steps_of evec

step.1 < horizon_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
DIV: horizon_of evec %| A + 1
MOD0: (A + 1) %% horizon_of evec = 0
vec:= value_at evec: duration -> nat
GT1: 1 < horizon_of evec
NOINF: value_at evec 0 = 0
step: Datatypes_prod__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality
IN: step \in steps_of evec

step.1 \in get_time_steps_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
DIV: horizon_of evec %| A + 1
MOD0: (A + 1) %% horizon_of evec = 0
vec:= value_at evec: duration -> nat
GT1: 1 < horizon_of evec
NOINF: value_at evec 0 = 0
step: Datatypes_prod__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality
IN: step \in steps_of evec

step.1 \in time_steps_of evec
by apply (map_f fst).
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

last (0, 0) [seq step <- steps_of evec | step.1 <= h.-1] = last (0, 0) (steps_of evec)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

[seq step <- steps_of evec | step.1 <= h.-1] = steps_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
DIV: horizon_of evec %| A + 1
MOD0: (A + 1) %% horizon_of evec = 0
vec:= value_at evec: duration -> nat
GT1: 1 < horizon_of evec
NOINF: value_at evec 0 = 0
step: Datatypes_prod__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality
IN: step \in steps_of evec

step.1 <= (horizon_of evec).-1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
DIV: horizon_of evec %| A + 1
MOD0: (A + 1) %% horizon_of evec = 0
vec:= value_at evec: duration -> nat
GT1: 1 < horizon_of evec
NOINF: value_at evec 0 = 0
step: Datatypes_prod__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality
IN: step \in steps_of evec
VALID: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < horizon_of evec

step.1 <= (horizon_of evec).-1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
DIV: horizon_of evec %| A + 1
MOD0: (A + 1) %% horizon_of evec = 0
vec:= value_at evec: duration -> nat
GT1: 1 < horizon_of evec
NOINF: value_at evec 0 = 0
step: Datatypes_prod__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality
IN: step \in steps_of evec
VALID: step.1 \in get_time_steps_of_task tsk -> step.1 < horizon_of evec

step.1 <= (horizon_of evec).-1
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
DIV: horizon_of evec %| A + 1
MOD0: (A + 1) %% horizon_of evec = 0
vec:= value_at evec: duration -> nat
GT1: 1 < horizon_of evec
NOINF: value_at evec 0 = 0
step: Datatypes_prod__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality Datatypes_nat__canonical__eqtype_Equality
IN: step \in steps_of evec
VALID: step.1 < horizon_of evec

step.1 <= (horizon_of evec).-1
by destruct (horizon_of evec).
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

A %/ h * vec h + vec h = (A + 1) %/ h * vec h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0

0 < (A + 1) %/ h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
GT1: 1 < h
NOINF: value_at evec 0 = 0
k: nat
EQk: A + 1 = k * h

0 < (k * h) %/ h
by destruct k;[lia | rewrite mulnK].
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
LT1: h < 1

A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
EQ1: 1 = h
A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
LT1: h < 1

A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
replace h with 0; rewrite /positive_horizon in POSh; lia.
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
EQ1: 1 = h

A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
EQ1: 1 = h

A %/ h * vec h + vec (A %% h) = (A + 1) %/ h * vec h + vec ((A + 1) %% h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
EQ1: 1 = h

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
EQ1: 1 = h
LTH: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in time_steps_of evec -> s < get_horizon_of_task tsk

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
EQ1: 1 = h
LTH: 1 < get_horizon_of_task tsk

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
evec: ArrivalCurvePrefix
EMAX: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
A: nat
h:= horizon_of evec: duration
DIV: h %| A + 1
MOD0: (A + 1) %% h = 0
vec:= value_at evec: duration -> nat
EQ1: 1 = h

get_horizon_of_task tsk <= 1
by unfold h in *; rewrite /get_horizon_of_task EMAX -EQ1. } Qed. (** Finally, we show that steps in the request-bound function correspond to points in the search space for fixed-priority tasks. *)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall A : nat, A < L -> task_rbf tsk A != task_rbf tsk (A + 1) -> A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts

forall A : nat, A < L -> task_rbf tsk A != task_rbf tsk (A + 1) -> A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)

A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false

A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false

(exists (i : nat) (t : Datatypes_nat__canonical__eqtype_Equality), i < (L %/ get_horizon_of_task tsk).+1 /\ t \in get_time_steps_of_task tsk /\ A + 1 = i * get_horizon_of_task tsk + t) \/ (exists i : nat, i < (L %/ get_horizon_of_task tsk).+1 /\ A + 1 = i * get_horizon_of_task tsk) -> A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk

A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk

A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
EQh: last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk
A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk

A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
VALID: valid_arrivals tsk

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
VALID: valid_arrivals tsk

has_valid_arrival_curve_prefix tsk -> False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
VALID: valid_arrivals tsk
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
VALID: valid_arrivals tsk
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
IN: (concept.task_cost tsk != 0) && (extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1))

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
VALID: valid_arrivals tsk
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
VALID: valid_arrivals tsk
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
VALID: valid_arrivals tsk
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQmax: get_horizon_of_task tsk %| A + 1 -> max_arrivals tsk A = max_arrivals tsk (A + 1)

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
VALID: valid_arrivals tsk
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQmax: max_arrivals tsk A = max_arrivals tsk (A + 1)

False
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
LTh: forall s : Datatypes_nat__canonical__eqtype_Equality, s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk
VALID: valid_arrivals tsk
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec
NEQ: extrapolated_arrival_curve evec A != extrapolated_arrival_curve evec (A + 1)
SORT_LEQ: sorted_leq_steps evec
EQmax: extrapolated_arrival_curve evec A = extrapolated_arrival_curve evec (A + 1)

False
by rewrite EQmax in NEQ; move: NEQ => /eqP.
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
EQh: last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk

A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
EQh: last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk

A \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
EQh: last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk

A + 1 - 1 \in search_space_arrival_curve_prefix_FP tsk L
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
DIV: (get_horizon_of_task tsk %| A) = false
i: nat
LT: i < (L %/ get_horizon_of_task tsk).+1
EQ: A + 1 = i * get_horizon_of_task tsk
EQh: last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk

i * get_horizon_of_task tsk \in repeat_steps_with_offset tsk [seq get_horizon_of_task tsk * i | i <- iota 0 (L %/ get_horizon_of_task tsk).+1]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h

i * h \in repeat_steps_with_offset tsk [seq h * i | i <- iota 0 (L %/ h).+1]
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h

i * h \in time_steps_with_offset tsk ((i - 1) * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h

h + (i - 1) * h = i * h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h
h + (i - 1) * h \in time_steps_with_offset tsk ((i - 1) * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h

h + (i - 1) * h = i * h
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h
POS: 0 < i

h + (i - 1) * h = i * h
by rewrite mulnBl mul1n; apply subnKC, leq_pmull.
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h

h + (i - 1) * h \in time_steps_with_offset tsk ((i - 1) * h)
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h

h \in get_time_steps_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h

last0 (get_time_steps_of_task tsk) \in get_time_steps_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h

has_valid_arrival_curve_prefix tsk -> last0 (get_time_steps_of_task tsk) \in get_time_steps_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: specified_bursts evec
SORT: sorted_ltn_steps evec

last0 (get_time_steps_of_task tsk) \in get_time_steps_of_task tsk
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
BUR: 1 \in time_steps_of evec
SORT: sorted_ltn_steps evec

last0 (time_steps_of evec) \in time_steps_of evec
L: duration
ts: seq Task
H_valid_task_set: task_set_with_valid_arrivals ts
tsk: Task
H_positive_cost: 0 < task_cost tsk
H_tsk_in_ts: tsk \in ts
A: nat
LT_L: A < L
IN: task_rbf tsk A != task_rbf tsk (A + 1)
h:= get_horizon_of_task tsk: duration
DIV: (h %| A) = false
i: nat
LT: i < (L %/ h).+1
EQ: A + 1 = i * h
EQh: last0 (get_time_steps_of_task tsk) = h
evec: ArrivalCurvePrefix
EMAXeq: get_arrival_curve_prefix tsk = evec
POSh: positive_horizon evec
LARGEh: large_horizon evec
NOINF: no_inf_arrivals evec
d: duration
l: seq duration
BUR: 1 \in d :: l
SORT: sorted_ltn_steps evec

last0 (d :: l) \in d :: l
by rewrite /last0 //=; apply mem_last. } Qed. End Facts. End FastSearchSpaceComputation.