Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Import prosa.util.all .Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.model.task.arrival.sporadic.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.model.task_arrivals.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * Sporadic Arrival Bound *)
(** In the following, we upper bound the number of jobs that can
arrive in any interval as constrained by the sporadic task model's
minimum inter-arrival time [task_min_inter_arrival_time]. *)
Section SporadicArrivalBound .
(** Consider any sporadic tasks ... *)
Context {Task : TaskType} `{SporadicModel Task}.
(** ... and their jobs. *)
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
(** We define the classic "ceiling of the interval length divided by
minimum inter-arrival time", which we prove to be correct in the
following. *)
Definition max_sporadic_arrivals (tsk : Task) (delta : duration) :=
div_ceil delta (task_min_inter_arrival_time tsk).
(** To establish the bound's soundness, consider any well-formed
arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any valid sporadic task [tsk] to be analyzed. *)
Variable tsk : Task.
Hypothesis H_sporadic_model : respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk.
(** Before we can establish the bound, we require two auxiliary
bounds, which we derive next. First, we consider minimum offset
of the <<n-th>> job of the task that arrives in a given interval. *)
Section NthJob .
(** For technical reasons, we require a "dummy" job in scope to
use the [nth] function. In the proofs, we establish that the
[dummy] job is never used, i.e., it is an irrelevant artifact
induced by the ssreflect API. It may be safely ignored. *)
Variable dummy : Job.
(** We observe that the <<i-th>> job to arrive in an interval <<[t1,t2)>>
arrives no earlier than [(task_min_inter_arrival_time tsk) *i]
time units after the beginning of the interval due the minimum
inter-arrival time of the sporadic task. *)
Lemma arrival_of_nth_job :
forall t1 t2 n i j ,
n = number_of_task_arrivals arr_seq tsk t1 t2 ->
i < n ->
j = nth dummy (task_arrivals_between arr_seq tsk t1 t2) i ->
job_arrival j >= t1 + (task_min_inter_arrival_time tsk) * i.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job
forall (t1 t2 : instant) (n i : nat) (j : Job),
n = number_of_task_arrivals arr_seq tsk t1 t2 ->
i < n ->
j =
nth dummy (task_arrivals_between arr_seq tsk t1 t2) i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j
Proof .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job
forall (t1 t2 : instant) (n i : nat) (j : Job),
n = number_of_task_arrivals arr_seq tsk t1 t2 ->
i < n ->
j =
nth dummy (task_arrivals_between arr_seq tsk t1 t2) i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j
move => t1 t2 n i j.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n, i : nat j : Job
n = number_of_task_arrivals arr_seq tsk t1 t2 ->
i < n ->
j =
nth dummy (task_arrivals_between arr_seq tsk t1 t2) i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j
rewrite /number_of_task_arrivals.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n, i : nat j : Job
n = size (task_arrivals_between arr_seq tsk t1 t2) ->
i < n ->
j =
nth dummy (task_arrivals_between arr_seq tsk t1 t2) i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j
case ARR : (task_arrivals_between arr_seq tsk t1 t2) => [|j' js'] -> // LIM JOB.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n, i : nat j, j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' LIM : i < size (j' :: js') JOB : j = nth dummy (j' :: js') i
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j
elim : i LIM j JOB => [LIM j JOB|i IH LIM j JOB].Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' LIM : 0 < size (j' :: js')j : Job JOB : j = nth dummy (j' :: js') 0
t1 + task_min_inter_arrival_time tsk * 0 <=
job_arrival j
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' LIM : 0 < size (j' :: js')j : Job JOB : j = nth dummy (j' :: js') 0
t1 + task_min_inter_arrival_time tsk * 0 <=
job_arrival j
rewrite muln0 addn0.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' LIM : 0 < size (j' :: js')j : Job JOB : j = nth dummy (j' :: js') 0
t1 <= job_arrival j
apply : job_arrival_between_ge; rt_eauto.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' LIM : 0 < size (j' :: js')j : Job JOB : j = nth dummy (j' :: js') 0
j \in arrivals_between arr_seq t1 ?Goal0
apply : (task_arrivals_between_subset _ tsk _ t2).Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' LIM : 0 < size (j' :: js')j : Job JOB : j = nth dummy (j' :: js') 0
j \in task_arrivals_between arr_seq tsk t1 t2
by rewrite JOB ARR; apply mem_nth. } Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1
t1 + task_min_inter_arrival_time tsk * i.+1 <=
job_arrival j
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1
t1 + task_min_inter_arrival_time tsk * i.+1 <=
job_arrival j
rewrite mulnSr addnA.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1
t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <= job_arrival j
pose prev_j := nth dummy (j' :: js') i.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job
t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <= job_arrival j
have prev_LIM : t1 + task_min_inter_arrival_time tsk * i + task_min_inter_arrival_time tsk
<= job_arrival prev_j + task_min_inter_arrival_time tsk
by rewrite leq_add2r; apply IH => //; lia .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk
t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <= job_arrival j
apply : (leq_trans prev_LIM).Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk
job_arrival prev_j + task_min_inter_arrival_time tsk <=
job_arrival j
have IN_j : j \in task_arrivals_between arr_seq tsk t1 t2
by rewrite JOB ARR; apply mem_nth.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2
job_arrival prev_j + task_min_inter_arrival_time tsk <=
job_arrival j
have IN_prev : prev_j \in task_arrivals_between arr_seq tsk t1 t2
by rewrite /prev_j ARR; apply mem_nth; lia .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
job_arrival prev_j + task_min_inter_arrival_time tsk <=
job_arrival j
apply : H_sporadic_model => //=.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
prev_j <> j
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
prev_j <> j
rewrite JOB /prev_j => /eqP.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
nth dummy (j' :: js') i == nth dummy (j' :: js') i.+1 ->
False
rewrite nth_uniq; try lia ; rewrite -ARR.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
uniq (task_arrivals_between arr_seq tsk t1 t2)
by apply : task_arrivals_between_uniq;rt_eauto. } Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
arrives_in arr_seq prev_j
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
arrives_in arr_seq prev_j
by apply /in_arrivals_implies_arrived/(task_arrivals_between_subset _ tsk t1 t2). } Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
arrives_in arr_seq j
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
arrives_in arr_seq j
by apply /in_arrivals_implies_arrived/(task_arrivals_between_subset _ tsk t1 t2). } Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
job_task prev_j = tsk
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
job_task prev_j = tsk
apply : in_task_arrivals_between_implies_job_of_task.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
prev_j
\in task_arrivals_between ?Goal1 tsk ?Goal2 ?Goal3
exact IN_prev. } Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
job_task j = tsk
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
job_task j = tsk
apply : in_task_arrivals_between_implies_job_of_task.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
j \in task_arrivals_between ?Goal0 tsk ?Goal1 ?Goal2
exact : IN_j. } Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
job_arrival prev_j <= job_arrival j
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
job_arrival prev_j <= job_arrival j
rewrite /prev_j JOB.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2
job_arrival (nth dummy (j' :: js') i) <=
job_arrival (nth dummy (j' :: js') i.+1 )
have SORTED : sorted by_arrival_times (j' :: js')
by rewrite -ARR; apply task_arrivals_between_sorted; rt_eauto.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2 SORTED : sorted by_arrival_times (j' :: js')
job_arrival (nth dummy (j' :: js') i) <=
job_arrival (nth dummy (j' :: js') i.+1 )
eapply (sorted_leq_nth _ _ _ SORTED); try lia .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2 SORTED : sorted by_arrival_times (j' :: js')
i \in [pred n | n < size (j' :: js')]
- Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2 SORTED : sorted by_arrival_times (j' :: js')
i \in [pred n | n < size (j' :: js')]
rewrite unfold_in simpl_predE; lia .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2 SORTED : sorted by_arrival_times (j' :: js')
i.+1 \in [pred n | n < size (j' :: js')]
- Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2 SORTED : sorted by_arrival_times (j' :: js')
i.+1 \in [pred n | n < size (j' :: js')]
rewrite unfold_in simpl_predE; lia . } }
Unshelve .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk dummy : Job t1, t2 : instant n : nat j' : Job js' : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j' :: js' i : nat IH : i < size (j' :: js') ->
forall j : Job,
j = nth dummy (j' :: js') i ->
t1 + task_min_inter_arrival_time tsk * i <=
job_arrival j LIM : i.+1 < size (j' :: js') j : Job JOB : j = nth dummy (j' :: js') i.+1 prev_j := nth dummy (j' :: js') i : Job prev_LIM : t1 + task_min_inter_arrival_time tsk * i +
task_min_inter_arrival_time tsk <=
job_arrival prev_j +
task_min_inter_arrival_time tsk IN_j : j \in task_arrivals_between arr_seq tsk t1 t2 IN_prev : prev_j
\in task_arrivals_between arr_seq tsk t1
t2 SORTED : sorted by_arrival_times (j' :: js')
transitive (T:=Job) by_arrival_times
all : by rewrite /by_arrival_times/transitive/reflexive; lia .
Qed .
End NthJob .
(** As a second auxiliary lemma, we establish a minimum length on
the interval for a given number of arrivals by applying the
previous lemma to the last job in the interval. We consider only
the case of "many" jobs, i.e., [n >= 2], which ensures that the
interval <<[t1, t2)>> spans at least one inter-arrival time. *)
Lemma minimum_distance_for_n_sporadic_arrivals :
forall t1 t2 n ,
number_of_task_arrivals arr_seq tsk t1 t2 = n ->
n >= 2 ->
t2 > t1 + (task_min_inter_arrival_time tsk) * n.-1 .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk
forall (t1 t2 : instant) (n : nat),
number_of_task_arrivals arr_seq tsk t1 t2 = n ->
1 < n ->
t1 + task_min_inter_arrival_time tsk * n.-1 < t2
Proof .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk
forall (t1 t2 : instant) (n : nat),
number_of_task_arrivals arr_seq tsk t1 t2 = n ->
1 < n ->
t1 + task_min_inter_arrival_time tsk * n.-1 < t2
move => t1 t2 n H_num_arrivals H_many_jobs.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < n
t1 + task_min_inter_arrival_time tsk * n.-1 < t2
(* First, let us get ourselves a job so we can discharge the dummy job parameter. *)
destruct (task_arrivals_between arr_seq tsk t1 t2) as [|j js] eqn :ARR;
first by move : ARR H_num_arrivals H_many_jobs; rewrite /number_of_task_arrivals => -> //= ->; lia .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js
t1 + task_min_inter_arrival_time tsk * n.-1 < t2
(* Now that we can use [nth], let's proceed with the actual proof. *)
set j_last := (nth j (task_arrivals_between arr_seq tsk t1 t2) n.-1 ).Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job
t1 + task_min_inter_arrival_time tsk * n.-1 < t2
have LAST : job_arrival j_last < t2.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job
job_arrival j_last < t2
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job
job_arrival j_last < t2
apply : job_arrival_between_lt; rt_eauto.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job
j_last \in arrivals_between arr_seq ?Goal0 t2
apply : task_arrivals_between_subset.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job
j_last
\in task_arrivals_between arr_seq ?Goal1 ?Goal0 t2
apply mem_nth.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job
n.-1 < size (task_arrivals_between arr_seq tsk t1 t2)
by move : H_num_arrivals; rewrite /number_of_task_arrivals => ->; lia . } Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job LAST : job_arrival j_last < t2
t1 + task_min_inter_arrival_time tsk * n.-1 < t2
have DIST : t1 + task_min_inter_arrival_time tsk * n.-1 <= job_arrival j_last.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job LAST : job_arrival j_last < t2
t1 + task_min_inter_arrival_time tsk * n.-1 <=
job_arrival j_last
{ Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job LAST : job_arrival j_last < t2
t1 + task_min_inter_arrival_time tsk * n.-1 <=
job_arrival j_last
apply : arrival_of_nth_job; auto ;
first by rewrite [number_of_task_arrivals arr_seq tsk t1 _]H_num_arrivals; lia .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job LAST : job_arrival j_last < t2
j_last =
nth ?Goal0
(task_arrivals_between arr_seq tsk t1 ?Goal1 ) n.-1
by rewrite /j_last //=. } Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat H_num_arrivals : number_of_task_arrivals arr_seq tsk
t1 t2 = n H_many_jobs : 1 < nj : Job js : seq Job ARR : task_arrivals_between arr_seq tsk t1 t2 =
j :: js j_last := nth j
(task_arrivals_between arr_seq tsk t1 t2)
n.-1 : Job LAST : job_arrival j_last < t2 DIST : t1 + task_min_inter_arrival_time tsk * n.-1 <=
job_arrival j_last
t1 + task_min_inter_arrival_time tsk * n.-1 < t2
by lia .
Qed .
(** Based on the above lemma, it is easy to see that
[max_sporadic_arrivals] is indeed a correct upper bound on the
maximum number of arrivals in a given interval. *)
Theorem sporadic_task_arrivals_bound :
forall t1 t2 ,
number_of_task_arrivals arr_seq tsk t1 t2 <= max_sporadic_arrivals tsk (t2 - t1).Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk
forall t1 t2 : instant,
number_of_task_arrivals arr_seq tsk t1 t2 <=
max_sporadic_arrivals tsk (t2 - t1)
Proof .Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk
forall t1 t2 : instant,
number_of_task_arrivals arr_seq tsk t1 t2 <=
max_sporadic_arrivals tsk (t2 - t1)
move => t1 t2.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant
number_of_task_arrivals arr_seq tsk t1 t2 <=
max_sporadic_arrivals tsk (t2 - t1)
case COUNT: (number_of_task_arrivals arr_seq tsk t1 t2) => // [n'].Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n' : nat COUNT : number_of_task_arrivals arr_seq tsk t1 t2 =
n'.+1
n' < max_sporadic_arrivals tsk (t2 - t1)
case COUNT: n' COUNT => // [|n] NARR.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n' : nat COUNT : n' = 0 NARR : number_of_task_arrivals arr_seq tsk t1 t2 = 1
0 < max_sporadic_arrivals tsk (t2 - t1)
{ (* one arrival *) Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n' : nat COUNT : n' = 0 NARR : number_of_task_arrivals arr_seq tsk t1 t2 = 1
0 < max_sporadic_arrivals tsk (t2 - t1)
apply div_ceil_gt0 => //; rewrite subn_gt0.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n' : nat COUNT : n' = 0 NARR : number_of_task_arrivals arr_seq tsk t1 t2 = 1
t1 < t2
by eapply number_of_task_arrivals_nonzero; eauto . } Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n', n : nat COUNT : n' = n.+1 NARR : number_of_task_arrivals arr_seq tsk t1 t2 =
n.+2
n.+1 < max_sporadic_arrivals tsk (t2 - t1)
{ (* two or more arrivals *) Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n', n : nat COUNT : n' = n.+1 NARR : number_of_task_arrivals arr_seq tsk t1 t2 =
n.+2
n.+1 < max_sporadic_arrivals tsk (t2 - t1)
clear n' COUNT.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat NARR : number_of_task_arrivals arr_seq tsk t1 t2 =
n.+2
n.+1 < max_sporadic_arrivals tsk (t2 - t1)
move : NARR.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat
number_of_task_arrivals arr_seq tsk t1 t2 = n.+2 ->
n.+1 < max_sporadic_arrivals tsk (t2 - t1)
set n' := n.+2 => NARR.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat n' := n.+2 : nat NARR : number_of_task_arrivals arr_seq tsk t1 t2 = n'
n' <= max_sporadic_arrivals tsk (t2 - t1)
have SEP: t2 > t1 + (task_min_inter_arrival_time tsk) * n'.-1
by apply : minimum_distance_for_n_sporadic_arrivals.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat n' := n.+2 : nat NARR : number_of_task_arrivals arr_seq tsk t1 t2 = n' SEP : t1 + task_min_inter_arrival_time tsk * n'.-1 <
t2
n' <= max_sporadic_arrivals tsk (t2 - t1)
move : SEP.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat n' := n.+2 : nat NARR : number_of_task_arrivals arr_seq tsk t1 t2 = n'
t1 + task_min_inter_arrival_time tsk * n'.-1 < t2 ->
n' <= max_sporadic_arrivals tsk (t2 - t1)
rewrite -ltn_subRL => SEP.Task : TaskType H : SporadicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk t1, t2 : instant n : nat n' := n.+2 : nat NARR : number_of_task_arrivals arr_seq tsk t1 t2 = n' SEP : task_min_inter_arrival_time tsk * n'.-1 <
t2 - t1
n' <= max_sporadic_arrivals tsk (t2 - t1)
by apply : div_ceil_multiple. }
Qed .
End SporadicArrivalBound .