Require Export prosa.analysis.definitions.hyperperiod.
[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.facts.periodic.task_arrivals_size.
Require Export prosa.util.div_mod.
Require Export prosa.util.tactics.

(** In this file we prove some simple properties of hyperperiods of periodic tasks. *)
Section Hyperperiod.

  (** Consider any type of periodic tasks, ... *)
  Context {Task : TaskType} `{PeriodicModel Task}.

  (** ... any task set [ts], ... *)
  Variable ts : TaskSet Task.

  (** ... and any task [tsk] that belongs to this task set. *)
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts: tsk \in ts.

  (** A task set's hyperperiod is an integral multiple
      of each task's period in the task set. **)
  Lemma hyperperiod_int_mult_of_any_task:
    exists (k : nat),
      hyperperiod ts = k * task_period tsk.
Task: TaskType
H: PeriodicModel Task
ts: TaskSet Task
tsk: Task
H_tsk_in_ts: tsk \in ts
exists k : nat, hyperperiod ts = k * task_period tsk
  Proof.
Task: TaskType
H: PeriodicModel Task
ts: TaskSet Task
tsk: Task
H_tsk_in_ts: tsk \in ts
exists k : nat, hyperperiod ts = k * task_period tsk by apply/dvdnP; apply lcm_seq_is_mult_of_all_ints, map_f, H_tsk_in_ts. Qed.

End Hyperperiod.

(** In this section we show a property of hyperperiod in context
   of task sets with valid periods. *)
Section ValidPeriodsImplyPositiveHP.

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

  (** ... and any task set [ts] ... *)
  Variable ts : TaskSet Task.

  (** ... such that all tasks in [ts] have valid periods. *)
  Hypothesis H_valid_periods: valid_periods ts.

  (** We show that the hyperperiod of task set [ts]
   is positive. *)
  Lemma valid_periods_imply_pos_hp:
    hyperperiod ts > 0.
Task: TaskType
H: PeriodicModel Task
ts: TaskSet Task
H_valid_periods: valid_periods ts
0 < hyperperiod ts
  Proof.
Task: TaskType
H: PeriodicModel Task
ts: TaskSet Task
H_valid_periods: valid_periods ts
0 < hyperperiod ts
    apply all_pos_implies_lcml_pos.
Task: TaskType
H: PeriodicModel Task
ts: TaskSet Task
H_valid_periods: valid_periods ts
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in [seq task_period i | i <- ts] -> 0 < x
    move => b /mapP [x IN EQ]; subst b.
Task: TaskType
H: PeriodicModel Task
ts: TaskSet Task
H_valid_periods: valid_periods ts
x: Task
IN: x \in ts
0 < task_period x
    now apply H_valid_periods.
  Qed.

End ValidPeriodsImplyPositiveHP.

(** In this section we prove some lemmas about the hyperperiod
    in context of the periodic model. *)
Section PeriodicLemmas.

  (** Consider any type of tasks, ... *)
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.

  (** ... any type of jobs, ... *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

  (** ... and a consistent arrival sequence with non-duplicate arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** Consider a task set [ts] such that all tasks in
      [ts] have valid periods. *)
  Variable ts : TaskSet Task.
  Hypothesis H_valid_periods: valid_periods ts.

  (** Let [tsk] be any periodic task in [ts] with a valid offset and period. *)
  Variable tsk : Task.
  Hypothesis H_task_in_ts: tsk \in ts.
  Hypothesis H_valid_offset: valid_offset arr_seq tsk.
  Hypothesis H_valid_period: valid_period tsk.
  Hypothesis H_periodic_task: respects_periodic_task_model arr_seq tsk.

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

  (** Let [O_max] denote the maximum task offset in [ts] and let
   [HP] denote the hyperperiod of all tasks in [ts]. *)
  Let O_max := max_task_offset ts.
  Let HP := hyperperiod ts.

  (** We show that the job corresponding to any job [j1] in any other
      hyperperiod is of the same task as [j1]. *)
  Lemma corresponding_jobs_have_same_task:
    forall j1 j2,
      job_task (corresponding_job_in_hyperperiod ts arr_seq j1
               (starting_instant_of_corresponding_hyperperiod ts j2) (job_task j1)) = job_task j1.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
forall j1 j2 : Job,
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
  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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
forall j1 j2 : Job,
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    clear H_task_in_ts H_valid_period.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
forall j1 j2 : Job,
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    move=> j1 j2.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    set ARRIVALS := (task_arrivals_between arr_seq (job_task j1) (starting_instant_of_hyperperiod ts (job_arrival j2))
          (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)).
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
ARRIVALS:= task_arrivals_between arr_seq 
  (job_task j1)
  (starting_instant_of_hyperperiod ts
     (job_arrival j2))
  (starting_instant_of_hyperperiod ts
     (job_arrival j2) + HP): seq Job
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    set IND := (job_index_in_hyperperiod ts arr_seq j1 (starting_instant_of_hyperperiod ts (job_arrival j1)) (job_task j1)).
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
ARRIVALS:= task_arrivals_between arr_seq 
  (job_task j1)
  (starting_instant_of_hyperperiod ts
     (job_arrival j2))
  (starting_instant_of_hyperperiod ts
     (job_arrival j2) + HP): seq Job
IND:= job_index_in_hyperperiod ts arr_seq j1
  (starting_instant_of_hyperperiod ts
     (job_arrival j1)) (job_task j1): nat
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    have SIZE_G : size ARRIVALS <= IND -> job_task (nth j1 ARRIVALS IND) = job_task j1 by intro SG; rewrite nth_default.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
ARRIVALS:= task_arrivals_between arr_seq 
  (job_task j1)
  (starting_instant_of_hyperperiod ts
     (job_arrival j2))
  (starting_instant_of_hyperperiod ts
     (job_arrival j2) + HP): seq Job
IND:= job_index_in_hyperperiod ts arr_seq j1
  (starting_instant_of_hyperperiod ts
     (job_arrival j1)) (job_task j1): nat
SIZE_G: size ARRIVALS <= IND ->
job_task (nth j1 ARRIVALS IND) = job_task j1
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    case: (boolP (size ARRIVALS == IND)) => [/eqP EQ|NEQ]; first by apply SIZE_G; 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
ARRIVALS:= task_arrivals_between arr_seq 
  (job_task j1)
  (starting_instant_of_hyperperiod ts
     (job_arrival j2))
  (starting_instant_of_hyperperiod ts
     (job_arrival j2) + HP): seq Job
IND:= job_index_in_hyperperiod ts arr_seq j1
  (starting_instant_of_hyperperiod ts
     (job_arrival j1)) (job_task j1): nat
SIZE_G: size ARRIVALS <= IND ->
job_task (nth j1 ARRIVALS IND) = job_task j1
NEQ: size ARRIVALS != IND
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    move : NEQ; rewrite neq_ltn; move => /orP [LT | G]; first by apply SIZE_G; 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
ARRIVALS:= task_arrivals_between arr_seq 
  (job_task j1)
  (starting_instant_of_hyperperiod ts
     (job_arrival j2))
  (starting_instant_of_hyperperiod ts
     (job_arrival j2) + HP): seq Job
IND:= job_index_in_hyperperiod ts arr_seq j1
  (starting_instant_of_hyperperiod ts
     (job_arrival j1)) (job_task j1): nat
SIZE_G: size ARRIVALS <= IND ->
job_task (nth j1 ARRIVALS IND) = job_task j1
G: IND < size ARRIVALS
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    set jb := nth j1 ARRIVALS 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
ARRIVALS:= task_arrivals_between arr_seq 
  (job_task j1)
  (starting_instant_of_hyperperiod ts
     (job_arrival j2))
  (starting_instant_of_hyperperiod ts
     (job_arrival j2) + HP): seq Job
IND:= job_index_in_hyperperiod ts arr_seq j1
  (starting_instant_of_hyperperiod ts
     (job_arrival j1)) (job_task j1): nat
SIZE_G: size ARRIVALS <= IND ->
job_task (nth j1 ARRIVALS IND) = job_task j1
G: IND < size ARRIVALS
jb:= nth j1 ARRIVALS IND: Job
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    have JOB_IN : jb \in ARRIVALS by apply mem_nth.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
ARRIVALS:= task_arrivals_between arr_seq 
  (job_task j1)
  (starting_instant_of_hyperperiod ts
     (job_arrival j2))
  (starting_instant_of_hyperperiod ts
     (job_arrival j2) + HP): seq Job
IND:= job_index_in_hyperperiod ts arr_seq j1
  (starting_instant_of_hyperperiod ts
     (job_arrival j1)) (job_task j1): nat
SIZE_G: size ARRIVALS <= IND ->
job_task (nth j1 ARRIVALS IND) = job_task j1
G: IND < size ARRIVALS
jb:= nth j1 ARRIVALS IND: Job
JOB_IN: jb \in ARRIVALS
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    rewrite /ARRIVALS /task_arrivals_between mem_filter in JOB_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
ARRIVALS:= task_arrivals_between arr_seq 
  (job_task j1)
  (starting_instant_of_hyperperiod ts
     (job_arrival j2))
  (starting_instant_of_hyperperiod ts
     (job_arrival j2) + HP): seq Job
IND:= job_index_in_hyperperiod ts arr_seq j1
  (starting_instant_of_hyperperiod ts
     (job_arrival j1)) (job_task j1): nat
SIZE_G: size ARRIVALS <= IND ->
job_task (nth j1 ARRIVALS IND) = job_task j1
G: IND < size ARRIVALS
jb:= nth j1 ARRIVALS IND: Job
JOB_IN: job_of_task (job_task j1) jb &&
(jb
   \in arrivals_between arr_seq
         (starting_instant_of_hyperperiod ts
            (job_arrival j2))
         (starting_instant_of_hyperperiod ts
            (job_arrival j2) + HP))
job_task
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) (job_task j1)) = job_task j1
    now move : JOB_IN => /andP [/eqP TSK JB_IN].
  Qed.

  (** We show that if a job [j] lies in the hyperperiod starting
   at instant [t] then [j] arrives in the interval <<[t, t + HP)>>. *)
  Lemma all_jobs_arrive_within_hyperperiod:
    forall j t,
      j \in jobs_in_hyperperiod ts arr_seq t tsk->
      t <= job_arrival j < t + HP.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
forall (j : Job) (t : instant),
j \in jobs_in_hyperperiod ts arr_seq t tsk ->
t <= job_arrival j < t + HP
  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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
forall (j : Job) (t : instant),
j \in jobs_in_hyperperiod ts arr_seq t tsk ->
t <= job_arrival j < t + HP
    intros * JB_IN_HP.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j: Job
t: instant
JB_IN_HP: j \in jobs_in_hyperperiod ts arr_seq t tsk
t <= job_arrival j < t + HP
    rewrite mem_filter in JB_IN_HP.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j: Job
t: instant
JB_IN_HP: job_of_task tsk j &&
(j
   \in arrivals_between arr_seq t
         (t + hyperperiod ts))
t <= job_arrival j < t + HP
    move : JB_IN_HP => /andP [/eqP TSK JB_IN]; apply mem_bigcat_nat_exists in JB_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j: Job
t: instant
TSK: job_task j = tsk
JB_IN: exists i : nat,
  j \in arrivals_at arr_seq i /\
  t <= i < t + hyperperiod ts
t <= job_arrival j < t + HP
    destruct JB_IN as [i [JB_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j: Job
t: instant
TSK: job_task j = tsk
i: nat
JB_IN: j \in arrivals_at arr_seq i
INEQ: t <= i < t + hyperperiod ts
t <= job_arrival j < t + HP
    apply job_arrival_at in JB_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j: Job
t: instant
TSK: job_task j = tsk
i: nat
JB_IN: job_arrival j = i
INEQ: t <= i < t + hyperperiod ts
t <= job_arrival j < t + HP
    by rewrite JB_IN.
  Qed.

  (** We show that the number of jobs in a hyperperiod starting at [n1 * HP + O_max]
   is the same as the number of jobs in a hyperperiod starting at [n2 * HP + O_max] given
   that [n1] is less than or equal to [n2]. *)
  Lemma eq_size_hyp_lt:
    forall n1 n2,
      n1 <= n2 ->
      size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
      size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
forall n1 n2 : nat,
n1 <= n2 ->
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
forall n1 n2 : nat,
n1 <= n2 ->
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     tsk)
    move=> n1 n2 N1_LT.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     tsk)
    have -> : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
size
  (jobs_in_hyperperiod ts arr_seq 
     (n1 * HP + O_max) tsk) =
size
  (jobs_in_hyperperiod ts arr_seq
     (n1 * HP + O_max + (n2 - n1) * HP) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP by rewrite -[in LHS](subnKC N1_LT) mulnDl addnAC. }
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq
     (n1 * HP + O_max + (n2 - n1) * HP) tsk)
    destruct (hyperperiod_int_mult_of_any_task ts tsk H_task_in_ts) as [k HYP]; rewrite !/HP.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
k: nat
HYP: hyperperiod ts = k * task_period tsk
size
  (jobs_in_hyperperiod ts arr_seq
     (n1 * hyperperiod ts + O_max) tsk) =
size
  (jobs_in_hyperperiod ts arr_seq
     (n1 * hyperperiod ts + O_max +
      (n2 - n1) * hyperperiod ts) tsk)
    rewrite [in X in _ = size (_ (n1 * HP + O_max + _ * X) tsk)]HYP.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
k: nat
HYP: hyperperiod ts = k * task_period tsk
size
  (jobs_in_hyperperiod ts arr_seq
     (n1 * hyperperiod ts + O_max) tsk) =
size
  (jobs_in_hyperperiod ts arr_seq
     (n1 * HP + O_max +
      (n2 - n1) * (k * task_period tsk)) tsk)
    rewrite mulnA /HP /jobs_in_hyperperiod !size_of_task_arrivals_between.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
k: nat
HYP: hyperperiod ts = k * task_period tsk
\sum_(n1 * hyperperiod ts + O_max <= t < n1 *
                                         hyperperiod
                                           ts + O_max +
                                         hyperperiod
                                           ts)
   size (task_arrivals_at arr_seq tsk t) =
\sum_(n1 * hyperperiod ts + O_max +
      (n2 - n1) * k * task_period tsk <= t < n1 *
                                             hyperperiod
                                               ts +
                                             O_max +
                                             (n2 - n1) *
                                             k *
                                             task_period
                                               tsk +
                                             hyperperiod
                                               ts)
   size (task_arrivals_at arr_seq tsk t)
    erewrite big_sum_eq_in_eq_sized_intervals => //; intros g G_LT.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
k: nat
HYP: hyperperiod ts = k * task_period tsk
g: nat
G_LT: g < hyperperiod ts
size
  (task_arrivals_at arr_seq tsk
     (n1 * hyperperiod ts + O_max + g)) =
(fun t : nat => size (task_arrivals_at arr_seq tsk t))
  (n1 * hyperperiod ts + O_max +
   (n2 - n1) * k * task_period tsk + g)
    have OFF_G : task_offset tsk <= O_max by apply max_offset_g.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
k: nat
HYP: hyperperiod ts = k * task_period tsk
g: nat
G_LT: g < hyperperiod ts
OFF_G: task_offset tsk <= O_max
size
  (task_arrivals_at arr_seq tsk
     (n1 * hyperperiod ts + O_max + g)) =
size
  (task_arrivals_at arr_seq tsk
     (n1 * hyperperiod ts + O_max +
      (n2 - n1) * k * task_period tsk + g))
    have FG : forall v b n, v + b + n = v + n + b by intros *; 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
k: nat
HYP: hyperperiod ts = k * task_period tsk
g: nat
G_LT: g < hyperperiod ts
OFF_G: task_offset tsk <= O_max
FG: forall v b n : nat, v + b + n = v + n + b
size
  (task_arrivals_at arr_seq tsk
     (n1 * hyperperiod ts + O_max + g)) =
size
  (task_arrivals_at arr_seq tsk
     (n1 * hyperperiod ts + O_max +
      (n2 - n1) * k * task_period tsk + g))
    erewrite eq_size_of_task_arrivals_seperated_by_period => //; last 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
N1_LT: n1 <= n2
k: nat
HYP: hyperperiod ts = k * task_period tsk
g: nat
G_LT: g < hyperperiod ts
OFF_G: task_offset tsk <= O_max
FG: forall v b n : nat, v + b + n = v + n + b
size
  (task_arrivals_at arr_seq tsk
     (n1 * hyperperiod ts + O_max + g +
      ?n * task_period tsk)) =
size
  (task_arrivals_at arr_seq tsk
     (n1 * hyperperiod ts + O_max +
      (n2 - n1) * k * task_period tsk + g))
    by rewrite FG.
  Qed.

  (** We generalize the above lemma by lifting the condition on
   [n1] and [n2]. *)
  Lemma eq_size_of_arrivals_in_hyperperiod:
    forall n1 n2,
      size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
      size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
forall n1 n2 : nat,
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
forall n1 n2 : nat,
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     tsk)
    move=> n1 n2.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     tsk)
    case : (boolP (n1 == n2)) => [/eqP EQ | NEQ]; first by rewrite 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
NEQ: n1 != n2
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     tsk)
    move : NEQ; rewrite neq_ltn; move => /orP [LT | LT].
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
LT: n1 < n2
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
LT: n2 < n1
size
  (jobs_in_hyperperiod ts arr_seq 
     (n1 * HP + O_max) tsk) =
size
  (jobs_in_hyperperiod ts arr_seq 
     (n2 * HP + O_max) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
LT: n1 < n2
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     tsk) by apply eq_size_hyp_lt => //; 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
LT: n2 < n1
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     tsk) move : (eq_size_hyp_lt n2 n1) => EQ_S.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
n1, n2: nat
LT: n2 < n1
EQ_S: n2 <= n1 ->
size
  (jobs_in_hyperperiod ts arr_seq
     (n2 * HP + O_max) tsk) =
size
  (jobs_in_hyperperiod ts arr_seq
     (n1 * HP + O_max) tsk)
size
  (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max)
     tsk)
      by feed_n 1 EQ_S => //; lia.
  Qed.

  (** Consider any two jobs [j1] and [j2] that stem from the arrival sequence
   [arr_seq] such that [j1] is of task [tsk]. *)
  Variable j1 : Job.
  Variable j2 : Job.
  Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
  Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
  Hypothesis H_j1_task: job_task j1 = tsk.

  (** Assume that both [j1] and [j2] arrive after [O_max]. *)
  Hypothesis H_j1_arr_after_O_max: O_max <= job_arrival j1.
  Hypothesis H_j2_arr_after_O_max: O_max <= job_arrival j2.

  (** We show that any job [j] that arrives in task arrivals in the same
      hyperperiod as [j2] also arrives in task arrivals up to [job_arrival j2 + HP]. *)
  Lemma job_in_hp_arrives_in_task_arrivals_up_to:
    forall j,
      j \in jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk ->
      j \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
forall j : Job,
j
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j2 - O_max) %/ HP * HP + O_max)
        tsk ->
j
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
  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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
forall j : Job,
j
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j2 - O_max) %/ HP * HP + O_max)
        tsk ->
j
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
    intros j J_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: j
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j2 - O_max) %/ HP * HP +
         O_max) tsk
j
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
    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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: j
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j2 - O_max) %/ HP * HP +
         O_max) tsk
j
  \in task_arrivals_between arr_seq tsk 0
        (job_arrival j2 + HP).+1
    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: j
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j2 - O_max) %/ HP * HP +
         O_max) tsk
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
j
  \in task_arrivals_between arr_seq tsk 0
        (job_arrival j2 + HP).+1
    move : (J_IN) => J_ARR; apply all_jobs_arrive_within_hyperperiod in J_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
J_ARR: j
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j2 - O_max) %/ HP * HP +
         O_max) tsk
j
  \in task_arrivals_between arr_seq tsk 0
        (job_arrival j2 + HP).+1
    rewrite /jobs_in_hp /jobs_in_hyperperiod /task_arrivals_up_to /task_arrivals_between mem_filter in J_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
J_ARR: job_of_task tsk j &&
(j
   \in arrivals_between arr_seq
         ((job_arrival j2 - O_max) %/ HP * HP +
          O_max)
         ((job_arrival j2 - O_max) %/ HP * HP +
          O_max + hyperperiod ts))
j
  \in task_arrivals_between arr_seq tsk 0
        (job_arrival j2 + HP).+1
    move : J_ARR =>  /andP [/eqP TSK' NTH_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
TSK': job_task j = tsk
NTH_IN: j
  \in arrivals_between arr_seq
        ((job_arrival j2 - O_max) %/ HP * HP +
         O_max)
        ((job_arrival j2 - O_max) %/ HP * HP +
         O_max + hyperperiod ts)
j
  \in task_arrivals_between arr_seq tsk 0
        (job_arrival j2 + HP).+1
    apply job_in_task_arrivals_between => //;
      first by apply in_arrivals_implies_arrived in NTH_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
TSK': job_task j = tsk
NTH_IN: j
  \in arrivals_between arr_seq
        ((job_arrival j2 - O_max) %/ HP * HP +
         O_max)
        ((job_arrival j2 - O_max) %/ HP * HP +
         O_max + hyperperiod ts)
0 <= job_arrival j < (job_arrival j2 + HP).+1
    apply mem_bigcat_nat_exists in NTH_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
TSK': job_task j = tsk
NTH_IN: exists i : nat,
  j \in arrivals_at arr_seq i /\
  (job_arrival j2 - O_max) %/ HP * HP + O_max <=
  i <
  (job_arrival j2 - O_max) %/ HP * HP + O_max +
  hyperperiod ts
0 <= job_arrival j < (job_arrival j2 + HP).+1
    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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
TSK': job_task j = tsk
NTH_IN: exists i : nat,
  j \in arrivals_at arr_seq i /\
  (job_arrival j2 - O_max) %/ HP * HP + O_max <=
  i <
  (job_arrival j2 - O_max) %/ HP * HP + O_max +
  hyperperiod ts
job_arrival j < (job_arrival j2 + HP).+1
    rewrite ltnS.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
TSK': job_task j = tsk
NTH_IN: exists i : nat,
  j \in arrivals_at arr_seq i /\
  (job_arrival j2 - O_max) %/ HP * HP + O_max <=
  i <
  (job_arrival j2 - O_max) %/ HP * HP + O_max +
  hyperperiod ts
job_arrival j <= job_arrival j2 + HP
    apply leq_trans with (n := (job_arrival j2 - O_max) %/ HP * HP + O_max + HP); 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
TSK': job_task j = tsk
NTH_IN: exists i : nat,
  j \in arrivals_at arr_seq i /\
  (job_arrival j2 - O_max) %/ HP * HP + O_max <=
  i <
  (job_arrival j2 - O_max) %/ HP * HP + O_max +
  hyperperiod ts
(job_arrival j2 - O_max) %/ HP * HP + O_max + HP <=
job_arrival j2 + HP
    rewrite leq_add2r.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
TSK': job_task j = tsk
NTH_IN: exists i : nat,
  j \in arrivals_at arr_seq i /\
  (job_arrival j2 - O_max) %/ HP * HP + O_max <=
  i <
  (job_arrival j2 - O_max) %/ HP * HP + O_max +
  hyperperiod ts
(job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j2
    have O_M : (job_arrival j2 - O_max) %/ HP * HP <= job_arrival j2 - O_max by apply leq_trunc_div.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
TSK': job_task j = tsk
NTH_IN: exists i : nat,
  j \in arrivals_at arr_seq i /\
  (job_arrival j2 - O_max) %/ HP * HP + O_max <=
  i <
  (job_arrival j2 - O_max) %/ HP * HP + O_max +
  hyperperiod ts
O_M: (job_arrival j2 - O_max) %/ HP * HP <=
job_arrival j2 - O_max
(job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j2
    have ARR_G : job_arrival j2 >= O_max 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j: Job
J_IN: (job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j <
(job_arrival j2 - O_max) %/ HP * HP + O_max +
HP
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
TSK': job_task j = tsk
NTH_IN: exists i : nat,
  j \in arrivals_at arr_seq i /\
  (job_arrival j2 - O_max) %/ HP * HP + O_max <=
  i <
  (job_arrival j2 - O_max) %/ HP * HP + O_max +
  hyperperiod ts
O_M: (job_arrival j2 - O_max) %/ HP * HP <=
job_arrival j2 - O_max
ARR_G: O_max <= job_arrival j2
(job_arrival j2 - O_max) %/ HP * HP + O_max <=
job_arrival j2
    lia.
  Qed.

  (** We show that job [j1] arrives in its own hyperperiod. *)
  Lemma job_in_own_hp:
    j1 \in jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP * HP + O_max) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j1
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j1 - O_max) %/ HP * HP + O_max)
        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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
j1
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j1 - O_max) %/ HP * HP + O_max)
        tsk
    apply job_in_task_arrivals_between => //.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
(job_arrival j1 - O_max) %/ HP * HP + O_max <=
job_arrival j1 <
(job_arrival j1 - O_max) %/ HP * HP + O_max +
hyperperiod ts
    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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
(job_arrival j1 - O_max) %/ HP * HP + O_max <=
job_arrival j1
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
job_arrival j1 <
(job_arrival j1 - O_max) %/ HP * HP + O_max +
hyperperiod ts
    +
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
(job_arrival j1 - O_max) %/ HP * HP + O_max <=
job_arrival j1 rewrite addnC -leq_subRL => //.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
(job_arrival j1 - O_max) %/ HP * HP <=
job_arrival j1 - O_max
      by apply leq_trunc_div.
    +
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
job_arrival j1 <
(job_arrival j1 - O_max) %/ HP * HP + O_max +
hyperperiod ts specialize (div_floor_add_g (job_arrival j1 - O_max) HP) => AB.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
AB: 0 < HP ->
job_arrival j1 - O_max <
(job_arrival j1 - O_max) %/ HP * HP + HP
job_arrival j1 <
(job_arrival j1 - O_max) %/ HP * HP + O_max +
hyperperiod ts
      feed_n 1 AB; first by apply valid_periods_imply_pos_hp => //.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
AB: job_arrival j1 - O_max <
(job_arrival j1 - O_max) %/ HP * HP + HP
job_arrival j1 <
(job_arrival j1 - O_max) %/ HP * HP + O_max +
hyperperiod ts
      rewrite ltn_subLR // in AB.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
AB: job_arrival j1 <
O_max +
((job_arrival j1 - O_max) %/ HP * HP + HP)
job_arrival j1 <
(job_arrival j1 - O_max) %/ HP * HP + O_max +
hyperperiod ts
      by rewrite -/(HP); lia.
  Qed.

  (** We show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod
   arrives in task arrivals up to [job_arrival j2 + HP]. *)
  Lemma corr_job_in_task_arrivals_up_to:
    corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk \in
      task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
corresponding_job_in_hyperperiod ts arr_seq j1
  (starting_instant_of_corresponding_hyperperiod ts j2)
  tsk
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
  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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
corresponding_job_in_hyperperiod ts arr_seq j1
  (starting_instant_of_corresponding_hyperperiod ts j2)
  tsk
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
    rewrite /corresponding_job_in_hyperperiod /starting_instant_of_corresponding_hyperperiod.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
nth j1
  (jobs_in_hyperperiod ts arr_seq
     (starting_instant_of_hyperperiod ts
        (job_arrival j2)) tsk)
  (job_index_in_hyperperiod ts arr_seq j1
     (starting_instant_of_hyperperiod ts
        (job_arrival j1)) tsk)
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
    rewrite /job_index_in_hyperperiod /starting_instant_of_hyperperiod /hyperperiod_index.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
nth j1
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j2 - max_task_offset ts)
      %/ hyperperiod ts * hyperperiod ts +
      max_task_offset ts) tsk)
  (index j1
     (jobs_in_hyperperiod ts arr_seq
        ((job_arrival j1 - max_task_offset ts)
         %/ hyperperiod ts * hyperperiod ts +
         max_task_offset ts) tsk))
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
    set ind := (index j1 (jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP * HP + O_max) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
ind:= index j1
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j1 - O_max) %/ HP * HP + O_max)
     tsk): nat
nth j1
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j2 - max_task_offset ts)
      %/ hyperperiod ts * hyperperiod ts +
      max_task_offset ts) tsk) ind
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
ind:= index j1
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j1 - O_max) %/ HP * HP + O_max)
     tsk): nat
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
nth j1 jobs_in_hp ind
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
    set nj := nth j1 jobs_in_hp 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
ind:= index j1
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j1 - O_max) %/ HP * HP + O_max)
     tsk): nat
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
nj:= nth j1 jobs_in_hp ind: Job
nj
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
    apply job_in_hp_arrives_in_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
ind:= index j1
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j1 - O_max) %/ HP * HP + O_max)
     tsk): nat
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
nj:= nth j1 jobs_in_hp ind: Job
nj
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j2 - O_max) %/ HP * HP + O_max)
        tsk
    rewrite mem_nth /jobs_in_hp => //.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
ind:= index j1
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j1 - O_max) %/ HP * HP + O_max)
     tsk): nat
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
nj:= nth j1 jobs_in_hp ind: Job
ind <
size
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk)
    specialize (eq_size_of_arrivals_in_hyperperiod ((job_arrival j2 - O_max) %/ HP) ((job_arrival j1 - O_max) %/ HP)) => 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
ind:= index j1
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j1 - O_max) %/ HP * HP + O_max)
     tsk): nat
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
nj:= nth j1 jobs_in_hp ind: Job
EQ: size
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j2 - O_max) %/ HP * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j1 - O_max) %/ HP * HP + O_max)
     tsk)
ind <
size
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk)
    rewrite EQ /ind index_mem.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
ind:= index j1
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j1 - O_max) %/ HP * HP + O_max)
     tsk): nat
jobs_in_hp:= jobs_in_hyperperiod ts arr_seq
  ((job_arrival j2 - O_max) %/ HP * HP +
   O_max) tsk: seq Job
nj:= nth j1 jobs_in_hp ind: Job
EQ: size
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j2 - O_max) %/ HP * HP + O_max)
     tsk) =
size
  (jobs_in_hyperperiod ts arr_seq
     ((job_arrival j1 - O_max) %/ HP * HP + O_max)
     tsk)
j1
  \in jobs_in_hyperperiod ts arr_seq
        ((job_arrival j1 - O_max) %/ HP * HP + O_max)
        tsk
    by apply job_in_own_hp.
  Qed.

  (** Finally, we show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod
   arrives in the arrival sequence [arr_seq]. *)
  Lemma corresponding_job_arrives:
      arrives_in arr_seq (corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
arrives_in arr_seq
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) 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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
arrives_in arr_seq
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) tsk)
    move : (corr_job_in_task_arrivals_up_to) => ARR_G.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
ARR_G: corresponding_job_in_hyperperiod ts arr_seq j1
  (starting_instant_of_corresponding_hyperperiod
     ts j2) tsk
  \in task_arrivals_up_to arr_seq tsk
        (job_arrival j2 + HP)
arrives_in arr_seq
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) tsk)
    rewrite /task_arrivals_up_to /task_arrivals_between mem_filter in ARR_G.
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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
ARR_G: job_of_task tsk
  (corresponding_job_in_hyperperiod ts arr_seq
     j1
     (starting_instant_of_corresponding_hyperperiod
        ts j2) tsk) &&
(corresponding_job_in_hyperperiod ts arr_seq
   j1
   (starting_instant_of_corresponding_hyperperiod
      ts j2) tsk
   \in arrivals_between arr_seq 0
         (job_arrival j2 + HP).+1)
arrives_in arr_seq
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) tsk)
    move : ARR_G =>  /andP [/eqP TSK' NTH_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
ts: TaskSet Task
H_valid_periods: valid_periods ts
tsk: Task
H_task_in_ts: tsk \in ts
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_periodic_task: respects_periodic_task_model arr_seq
  tsk
H_infinite_jobs: infinite_jobs arr_seq
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
j1, j2: Job
H_j1_from_arr_seq: arrives_in arr_seq j1
H_j2_from_arr_seq: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j1_arr_after_O_max: O_max <= job_arrival j1
H_j2_arr_after_O_max: O_max <= job_arrival j2
TSK': job_task
  (corresponding_job_in_hyperperiod ts arr_seq
     j1
     (starting_instant_of_corresponding_hyperperiod
        ts j2) tsk) = tsk
NTH_IN: corresponding_job_in_hyperperiod ts arr_seq
  j1
  (starting_instant_of_corresponding_hyperperiod
     ts j2) tsk
  \in arrivals_between arr_seq 0
        (job_arrival j2 + HP).+1
arrives_in arr_seq
  (corresponding_job_in_hyperperiod ts arr_seq j1
     (starting_instant_of_corresponding_hyperperiod ts
        j2) tsk)
    by apply in_arrivals_implies_arrived in NTH_IN.
  Qed.

End PeriodicLemmas.