Require Export prosa.analysis.facts.periodic.arrival_times.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.definitions.infinite_jobs.
Require Export prosa.analysis.facts.sporadic.arrival_sequence.

(** In this file we prove some properties concerning the size
 of task arrivals in context of the periodic model. *)
Section TaskArrivalsSize.

  (** Consider any type of periodic tasks with an offset ... *)
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.

  (** ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

  (** Consider any unique arrival sequence with consistent arrivals ... *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** ... and any periodic task [tsk] with a valid offset and period. *)
  Variable tsk : Task.
  Hypothesis H_valid_offset : valid_offset arr_seq tsk.
  Hypothesis H_valid_period : valid_period tsk.
  Hypothesis H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk.

  (** We show that if an instant [t] is not an "arrival time" for
      task [tsk] then [task_arrivals_at arr_seq tsk t] is an empty sequence. *)
  Lemma task_arrivals_size_at_non_arrival:
    forall t,
      (forall n, t <> task_offset tsk + n * task_period tsk) ->
      task_arrivals_at arr_seq tsk t = [::].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
forall t : nat,
(forall n : nat,
 t <> task_offset tsk + n * task_period tsk) ->
task_arrivals_at arr_seq tsk t = [::]
  Proof.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
forall t : nat,
(forall n : nat,
 t <> task_offset tsk + n * task_period tsk) ->
task_arrivals_at arr_seq tsk t = [::]
    move=> t T.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
task_arrivals_at arr_seq tsk t = [::]
    have EMPT_OR_EXISTS : forall xs, xs = [::] \/ exists a, a \in xs.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
task_arrivals_at arr_seq tsk t = [::]
    {
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs) move=> t0; elim=> [|a xs IHxs]; first by left.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
t0: eqType
a: t0
xs: seq t0
IHxs: xs = [::] \/ (exists a : t0, a \in xs)
a :: xs = [::] \/ (exists a0 : t0, a0 \in a :: xs)
      right; exists a.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
t0: eqType
a: t0
xs: seq t0
IHxs: xs = [::] \/ (exists a : t0, a \in xs)
a \in a :: xs
      by apply mem_head.
    }
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
task_arrivals_at arr_seq tsk t = [::]
    destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] => //.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a: Job
A_IN: a \in task_arrivals_at arr_seq tsk t
task_arrivals_at arr_seq tsk t = [::]
    rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN => /andP [/eqP TSK A_ARR].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
A_ARR: a \in arrivals_at arr_seq t
task_arrivals_at arr_seq tsk t = [::]
    move : H_valid_arrival_sequence => [CONSISTENT UNIQ].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
A_ARR: a \in arrivals_at arr_seq t
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
task_arrivals_at arr_seq tsk t = [::]
    move : (A_ARR) => A_IN; apply CONSISTENT in A_IN.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
T: forall n : nat,
t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
A_ARR: a \in arrivals_at arr_seq t
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
task_arrivals_at arr_seq tsk t = [::]
    rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat,
job_arrival a <>
task_offset tsk + n * task_period tsk
A_ARR: a \in arr_seq t
task_arrivals_at arr_seq tsk t = [::]
    apply in_arrseq_implies_arrives in A_ARR.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat,
job_arrival a <>
task_offset tsk + n * task_period tsk
A_ARR: arrives_in arr_seq a
task_arrivals_at arr_seq tsk t = [::]
    have EXISTS_N : exists n, job_arrival a = task_offset tsk + n * task_period tsk
        by exact: (job_arrival_times arr_seq).
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat,
job_arrival a <>
task_offset tsk + n * task_period tsk
A_ARR: arrives_in arr_seq a
EXISTS_N: exists n : nat,
  job_arrival a =
  task_offset tsk + n * task_period tsk
task_arrivals_at arr_seq tsk t = [::]
    move : EXISTS_N => [n A_ARRIVAL].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat,
job_arrival a <>
task_offset tsk + n * task_period tsk
A_ARR: arrives_in arr_seq a
n: nat
A_ARRIVAL: job_arrival a =
task_offset tsk + n * task_period tsk
task_arrivals_at arr_seq tsk t = [::]
    by move : (T n) => T1.
  Qed.

  (** We show that at any instant [t], at most one job of task [tsk]
      can arrive (i.e. size of [task_arrivals_at arr_seq tsk t] is at most one). *)
  Lemma task_arrivals_at_size_cases:
    forall t,
      size (task_arrivals_at arr_seq tsk t) = 0 \/
        size (task_arrivals_at arr_seq tsk t) = 1.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
forall t : instant,
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
  Proof.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
forall t : instant,
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    intro t.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) => [LT|GT|EQ];
         [by destruct (size (task_arrivals_at arr_seq tsk t)); left| |by lia].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    specialize (exists_two (task_arrivals_at arr_seq tsk t)) => EXISTS_TWO.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
EXISTS_TWO: 1 < size (task_arrivals_at arr_seq tsk t) ->
uniq (task_arrivals_at arr_seq tsk t) ->
exists a b : Job,
  a <> b /\
  a \in task_arrivals_at arr_seq tsk t /\
  b \in task_arrivals_at arr_seq tsk t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    move : H_valid_arrival_sequence => [CONSISTENT UNIQ].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
EXISTS_TWO: 1 < size (task_arrivals_at arr_seq tsk t) ->
uniq (task_arrivals_at arr_seq tsk t) ->
exists a b : Job,
  a <> b /\
  a \in task_arrivals_at arr_seq tsk t /\
  b \in task_arrivals_at arr_seq tsk t
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by [] | by apply filter_uniq | ].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
A_IN: a \in task_arrivals_at arr_seq tsk t
B_IN: b \in task_arrivals_at arr_seq tsk t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
A_IN: job_of_task tsk a &&
(a \in arrivals_at arr_seq t)
B_IN: job_of_task tsk b &&
(b \in arrivals_at arr_seq t)
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    move: A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    move: (ARRA); move: (ARRB); rewrite /arrivals_at => A_IN B_IN.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: b \in arr_seq t
B_IN: a \in arr_seq t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    have SPO : respects_sporadic_task_model arr_seq tsk => [//|].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
SPO: respects_sporadic_task_model arr_seq tsk
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    have EQ_ARR_A : (job_arrival a = t) by [].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
SPO: respects_sporadic_task_model arr_seq tsk
EQ_ARR_A: job_arrival a = t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    have EQ_ARR_B : (job_arrival b = t) by [].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
SPO: respects_sporadic_task_model arr_seq tsk
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    specialize (SPO a b); feed_n 6 SPO => //; first lia.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
SPO: job_arrival a + task_min_inter_arrival_time tsk <=
job_arrival b
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    rewrite EQ_ARR_A EQ_ARR_B in SPO.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t
SPO: t + task_min_inter_arrival_time tsk <= t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    rewrite /task_min_inter_arrival_time /periodic_as_sporadic in SPO.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t
SPO: t + task_period tsk <= t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    have POS : task_period tsk > 0 by [].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t
SPO: t + task_period tsk <= t
POS: 0 < task_period tsk
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
    lia.
  Qed.

  (** We show that the size of task arrivals (strictly) between two consecutive arrival
      times is zero. *)
  Lemma size_task_arrivals_between_eq0:
    forall n,
      let l := (task_offset tsk + n * task_period tsk).+1 in
      let r := (task_offset tsk + n.+1 * task_period tsk) in
      size (task_arrivals_between arr_seq tsk l r) = 0.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
forall n : nat,
let l := (task_offset tsk + n * task_period tsk).+1 in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_between arr_seq tsk l r) = 0
  Proof.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
forall n : nat,
let l := (task_offset tsk + n * task_period tsk).+1 in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_between arr_seq tsk l r) = 0
    intros n l r; rewrite /l /r.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
size
  (task_arrivals_between arr_seq tsk
     (task_offset tsk + n * task_period tsk).+1
     (task_offset tsk + n.+1 * task_period tsk)) = 0
    rewrite size_of_task_arrivals_between big_nat_eq0 => //; intros t INEQ.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t: nat
INEQ: task_offset tsk + n * task_period tsk < t <
task_offset tsk + n.+1 * task_period tsk
size (task_arrivals_at arr_seq tsk t) = 0
    rewrite task_arrivals_size_at_non_arrival => //; intros n1 EQ.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t: nat
INEQ: task_offset tsk + n * task_period tsk < t <
task_offset tsk + n.+1 * task_period tsk
n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk
False
    rewrite EQ in INEQ.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t, n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk
INEQ: task_offset tsk + n * task_period tsk <
task_offset tsk + n1 * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
False
    move : INEQ => /andP [INEQ1 INEQ2].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t, n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk
INEQ1: task_offset tsk + n * task_period tsk <
task_offset tsk + n1 * task_period tsk
INEQ2: task_offset tsk + n1 * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
False
    rewrite ltn_add2l ltn_mul2r in INEQ1; rewrite ltn_add2l ltn_mul2r in INEQ2.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t, n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk
INEQ1: (0 < task_period tsk) && (n < n1)
INEQ2: (0 < task_period tsk) && (n1 < n.+1)
False
    move : INEQ1 INEQ2 => /andP [A B] /andP [C D].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t, n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk
A: 0 < task_period tsk
B: n < n1
C: 0 < task_period tsk
D: n1 < n.+1
False
    by lia.
  Qed.

  (** In this section we show some properties of task arrivals in case
      of an infinite sequence of jobs. *)
  Section TaskArrivalsInCaseOfInfiniteJobs.

    (** Assume that we have an infinite sequence of jobs. *)
    Hypothesis H_infinite_jobs : infinite_jobs arr_seq.

    (** We show that for any number [n], there exists a job [j] of task [tsk]
        such that [job_index] of [j] is equal to [n] and [j] arrives
        at [task_offset tsk + n * task_period tsk]. *)
    Lemma jobs_exists_later:
      forall n,
      exists j,
        arrives_in arr_seq j /\
        job_task j = tsk /\
        job_arrival j = task_offset tsk + n * task_period tsk /\
        job_index arr_seq j = n.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
forall n : nat,
exists j : Job,
  arrives_in arr_seq j /\
  job_task j = tsk /\
  job_arrival j =
  task_offset tsk + n * task_period tsk /\
  job_index arr_seq j = n
    Proof.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
forall n : nat,
exists j : Job,
  arrives_in arr_seq j /\
  job_task j = tsk /\
  job_arrival j =
  task_offset tsk + n * task_period tsk /\
  job_index arr_seq j = n
      move=> n.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
exists j : Job,
  arrives_in arr_seq j /\
  job_task j = tsk /\
  job_arrival j =
  task_offset tsk + n * task_period tsk /\
  job_index arr_seq j = n
      destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
exists j : Job,
  arrives_in arr_seq j /\
  job_task j = tsk /\
  job_arrival j =
  task_offset tsk + n * task_period tsk /\
  job_index arr_seq j = n
      exists j; repeat split => //.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
job_arrival j = task_offset tsk + n * task_period tsk
      exact: (periodic_arrival_times arr_seq).
    Qed.

    (** We show that the size of task arrivals at any arrival time is equal to one. *)
    Lemma task_arrivals_at_size:
      forall n,
        let l := (task_offset tsk + n * task_period tsk) in
        size (task_arrivals_at arr_seq tsk l) = 1.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
    Proof.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
      intros n l; rewrite /l.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
l:= task_offset tsk + n * task_period tsk: nat
size
  (task_arrivals_at arr_seq tsk
     (task_offset tsk + n * task_period tsk)) = 1
      move : (jobs_exists_later n) => [j' [ARR [TSK [ARRIVAL IND]]]].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
l:= task_offset tsk + n * task_period tsk: nat
j': Job
ARR: arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' =
task_offset tsk + n * task_period tsk
IND: job_index arr_seq j' = n
size
  (task_arrivals_at arr_seq tsk
     (task_offset tsk + n * task_period tsk)) = 1
      apply (only_j_in_task_arrivals_at_j
               arr_seq H_valid_arrival_sequence tsk) in ARR => //.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
l:= task_offset tsk + n * task_period tsk: nat
j': Job
ARR: task_arrivals_at_job_arrival arr_seq j' =
[:: j']
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' =
task_offset tsk + n * task_period tsk
IND: job_index arr_seq j' = n
size
  (task_arrivals_at arr_seq tsk
     (task_offset tsk + n * task_period tsk)) = 1
      rewrite /task_arrivals_at_job_arrival TSK in ARR.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
l:= task_offset tsk + n * task_period tsk: nat
j': Job
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' =
task_offset tsk + n * task_period tsk
IND: job_index arr_seq j' = n
ARR: task_arrivals_at arr_seq tsk (job_arrival j') =
[:: j']
size
  (task_arrivals_at arr_seq tsk
     (task_offset tsk + n * task_period tsk)) = 1
      by rewrite -ARRIVAL ARR.
    Qed.

    (** We show that the size of task arrivals up to [task_offset tsk] is equal to one. *)
    Lemma size_task_arrivals_up_to_offset:
      size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
size
  (task_arrivals_up_to arr_seq tsk (task_offset tsk)) =
1
    Proof.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
size
  (task_arrivals_up_to arr_seq tsk (task_offset tsk)) =
1
      rewrite /task_arrivals_up_to.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk).+1) = 1
      specialize (task_arrivals_between_cat arr_seq tsk 0 (task_offset tsk) (task_offset tsk).+1) => CAT.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: 0 <= task_offset tsk ->
task_offset tsk <= (task_offset tsk).+1 ->
task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk).+1) = 1
      feed_n 2 CAT => //; rewrite CAT size_cat.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk)) +
size
  (task_arrivals_between arr_seq tsk (task_offset tsk)
     (task_offset tsk).+1) = 1
      have Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk)) = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
Z: size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk)) = 0
size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk)) +
size
  (task_arrivals_between arr_seq tsk 
     (task_offset tsk) 
     (task_offset tsk).+1) = 1
      {
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk)) = 0 rewrite size_of_task_arrivals_between big_nat_eq0 => //; intros t T_EQ.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
t: nat
T_EQ: 0 <= t < task_offset tsk
size (task_arrivals_at arr_seq tsk t) = 0
        rewrite task_arrivals_size_at_non_arrival => //; intros n EQ.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
t: nat
T_EQ: 0 <= t < task_offset tsk
n: nat
EQ: t = task_offset tsk + n * task_period tsk
False
        by lia.
      }
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
Z: size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk)) = 0
size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk)) +
size
  (task_arrivals_between arr_seq tsk (task_offset tsk)
     (task_offset tsk).+1) = 1
      rewrite Z add0n /task_arrivals_between /arrivals_between big_nat1.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
Z: size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk)) = 0
size
  [seq j <- arrivals_at arr_seq (task_offset tsk)
     | job_of_task tsk j] = 1
      specialize (task_arrivals_at_size 0) => AT_SIZE.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0
  (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
  (task_offset tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk) 
  (task_offset tsk).+1
Z: size
  (task_arrivals_between arr_seq tsk 0
     (task_offset tsk)) = 0
AT_SIZE: let l :=
  task_offset tsk + 0 * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
size
  [seq j <- arrivals_at arr_seq (task_offset tsk)
     | job_of_task tsk j] = 1
      by rewrite mul0n addn0 in AT_SIZE.
    Qed.

    (** We show that for any number [n], the number of jobs released by task [tsk] up to
        [task_offset tsk + n * task_period tsk] is equal to [n + 1]. *)
    Lemma task_arrivals_up_to_size:
      forall n,
        let l := (task_offset tsk + n * task_period tsk) in
        let r := (task_offset tsk + n.+1 * task_period tsk) in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
    Proof.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
      elim=> [|n IHn].
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
let l := task_offset tsk + 0 * task_period tsk in
let r := task_offset tsk + 1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = 0 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
let l := task_offset tsk + n.+1 * task_period tsk in
let r := task_offset tsk + n.+2 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
      -
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
let l := task_offset tsk + 0 * task_period tsk in
let r := task_offset tsk + 1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = 0 + 1 intros l r; rewrite /l mul0n add0n addn0.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
l:= task_offset tsk + 0 * task_period tsk: nat
r:= task_offset tsk + 1 * task_period tsk: nat
size
  (task_arrivals_up_to arr_seq tsk (task_offset tsk)) =
1
        by apply size_task_arrivals_up_to_offset.
      -
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
let l := task_offset tsk + n.+1 * task_period tsk in
let r := task_offset tsk + n.+2 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1 intros l r.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
        specialize (task_arrivals_cat arr_seq tsk (task_offset tsk + n * task_period tsk)
                      (task_offset tsk + n.+1 * task_period tsk)) => CAT.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_offset tsk + n * task_period tsk <=
task_offset tsk + n.+1 * task_period tsk ->
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
        feed_n 1 CAT; first by lia.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
        rewrite CAT size_cat IHn.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
n + 1 +
size
  (task_arrivals_between arr_seq tsk
     (task_offset tsk + n * task_period tsk).+1
     (task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
        specialize (task_arrivals_between_cat arr_seq tsk (task_offset tsk + n * task_period tsk).+1
                      (task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1) => S_CAT.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk)
  (task_offset tsk + n.+1 * task_period tsk).+1
n + 1 +
size
  (task_arrivals_between arr_seq tsk
     (task_offset tsk + n * task_period tsk).+1
     (task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
        feed_n 2 S_CAT; try by lia.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk)
  (task_offset tsk + n.+1 * task_period tsk).+1
task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk)
  (task_offset tsk + n.+1 * task_period tsk).+1
n + 1 +
size
  (task_arrivals_between arr_seq tsk
     (task_offset tsk + n * task_period tsk).+1
     (task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
        {
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk)
  (task_offset tsk + n.+1 * task_period tsk).+1
task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk rewrite ltn_add2l ltn_mul2r.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk)
  (task_offset tsk + n.+1 * task_period tsk).+1
(0 < task_period tsk) && (n < n.+1)
          by apply /andP; split => //.
        }
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk)
  (task_offset tsk + n.+1 * task_period tsk).+1
n + 1 +
size
  (task_arrivals_between arr_seq tsk
     (task_offset tsk + n * task_period tsk).+1
     (task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
        rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk)
  (task_offset tsk + n.+1 * task_period tsk).+1
n + 1 +
(size
   [seq j <- \cat_((task_offset tsk +
                    n * task_period tsk).+1<=t<task_offset
                                                 tsk +
                                               n.+1 *
                                               task_period
                                                 tsk)
              arrivals_at arr_seq t
      | job_of_task tsk j] +
 size
   [seq j <- arrivals_at arr_seq
               (task_offset tsk +
                n.+1 * task_period tsk)
      | job_of_task tsk j]) = n.+1 + 1
        rewrite size_task_arrivals_between_eq0 task_arrivals_at_size => //.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk
  in
let r :=
  task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
  (task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
  (task_offset tsk + n * task_period tsk).+1
  (task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
  (task_offset tsk + n.+1 * task_period tsk)
  (task_offset tsk + n.+1 * task_period tsk).+1
n + 1 + (0 + 1) = n.+1 + 1
        by lia.
    Qed.

    (** We show that the number of jobs released by task [tsk] at any instant [t]
        and [t + n * task_period tsk] is the same for any number [n]. *)
    Lemma eq_size_of_task_arrivals_seperated_by_period:
      forall n t,
        t >= task_offset tsk ->
        size (task_arrivals_at arr_seq tsk t) =
        size (task_arrivals_at arr_seq tsk (t + n * task_period tsk)).
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
forall n t : nat,
task_offset tsk <= t ->
size (task_arrivals_at arr_seq tsk t) =
size
  (task_arrivals_at arr_seq tsk
     (t + n * task_period tsk))
    Proof.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
forall n t : nat,
task_offset tsk <= t ->
size (task_arrivals_at arr_seq tsk t) =
size
  (task_arrivals_at arr_seq tsk
     (t + n * task_period tsk))
      move=> n t o_le_t.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
size (task_arrivals_at arr_seq tsk t) =
size
  (task_arrivals_at arr_seq tsk
     (t + n * task_period tsk))
      have [tmo_eq0|tmo_neq0] :=
        @eqP _ ((t - task_offset tsk) %% task_period tsk) 0.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_eq0: (t - task_offset tsk) %% task_period tsk = 0
size (task_arrivals_at arr_seq tsk t) =
size
  (task_arrivals_at arr_seq tsk
     (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <>
0
size (task_arrivals_at arr_seq tsk t) =
size
  (task_arrivals_at arr_seq tsk
     (t + n * task_period tsk))
      -
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_eq0: (t - task_offset tsk) %% task_period tsk = 0
size (task_arrivals_at arr_seq tsk t) =
size
  (task_arrivals_at arr_seq tsk
     (t + n * task_period tsk)) rewrite -(subnKC o_le_t) (divn_eq (t - _) (task_period tsk)).
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_eq0: (t - task_offset tsk) %% task_period tsk = 0
size
  (task_arrivals_at arr_seq tsk
     (task_offset tsk +
      ((t - task_offset tsk) %/ task_period tsk *
       task_period tsk +
       (t - task_offset tsk) %% task_period tsk))) =
size
  (task_arrivals_at arr_seq tsk
     (task_offset tsk +
      ((t - task_offset tsk) %/ task_period tsk *
       task_period tsk +
       (t - task_offset tsk) %% task_period tsk) +
      n * task_period tsk))
        by rewrite tmo_eq0 addn0 -addnA -mulnDl !task_arrivals_at_size.
      -
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <>
0
size (task_arrivals_at arr_seq tsk t) =
size
  (task_arrivals_at arr_seq tsk
     (t + n * task_period tsk)) rewrite !task_arrivals_size_at_non_arrival// => n';
        move=> /(f_equal (subn^~(task_offset tsk))); rewrite addKn;
        move=> /(f_equal (modn^~(task_period tsk))).
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <>
0
n': nat
t + n * task_period tsk - task_offset tsk
  = n' * task_period tsk
  %[mod task_period tsk] -> False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <>
0
n': nat
t - task_offset tsk
  = n' * task_period tsk
  %[mod task_period tsk] -> False
        +
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <>
0
n': nat
t + n * task_period tsk - task_offset tsk
  = n' * task_period tsk
  %[mod task_period tsk] -> False by rewrite -addnBAC// addnC -[n' * _]addn0 !modnMDl mod0n.
        +
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model
  arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <>
0
n': nat
t - task_offset tsk
  = n' * task_period tsk
  %[mod task_period tsk] -> False by rewrite -[n' * _]addn0 modnMDl mod0n.
    Qed.

  End TaskArrivalsInCaseOfInfiniteJobs.

End TaskArrivalsSize.