Require Import prosa.util.all.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.analysis.facts.model.task_arrivals.

(** * 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'
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'
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 => //.
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
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 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_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 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_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
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. }
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 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_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 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_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
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
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 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_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
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 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_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_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_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_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.
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.+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 \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')] 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
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')
reflexive (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 < n
j: 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 < n
j: 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 < n
j: 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 < n
j: 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
    {
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
j: 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 => //.
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
j: 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 < n
j: 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 < n
j: 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 < n
j: 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 < n
j: 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 < n
j: 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
    {
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
j: 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 < n
j: 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 []. }
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
j: 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
    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)
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)
    { (* 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.