Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** 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. **)
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
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. *)
Task: TaskType
H: PeriodicModel Task
ts: TaskSet Task
H_valid_periods: valid_periods ts

0 < hyperperiod ts
Task: TaskType
H: PeriodicModel Task
ts: TaskSet Task
H_valid_periods: valid_periods ts

0 < hyperperiod ts
Task: TaskType
H: PeriodicModel Task
ts: TaskSet Task
H_valid_periods: valid_periods ts

forall x : nat_eqType, x \in [seq task_period i | i <- ts] -> 0 < x
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_consistent_arrivals: consistent_arrival_times arr_seq. Hypothesis H_uniq_arr_seq: arrival_sequence_uniq 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]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)>>. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
now 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]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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))
now rewrite FG. Qed. (** We generalize the above lemma by lifting the condition on [n1] and [n2]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
now 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]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
i: nat
NJ_IN: job_arrival j = i
INEQ: (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts

0 <= job_arrival j < (job_arrival j2 + HP).+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
i: nat
NJ_IN: job_arrival j = i
INEQ: (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts

job_arrival j < (job_arrival j2 + HP).+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
i: nat
NJ_IN: job_arrival j = i
INEQ: (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts

job_arrival j <= 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
i: nat
NJ_IN: job_arrival j = i
INEQ: (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j < (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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
i: nat
NJ_IN: job_arrival j = i
INEQ: (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts

(job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j2
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
i: nat
NJ_IN: job_arrival j = i
INEQ: (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j < (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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
i: nat
NJ_IN: job_arrival j = i
INEQ: (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j < (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
now lia. Qed. (** We show that job [j1] arrives in its own hyperperiod. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
now 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]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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
now 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]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq 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)
now apply in_arrivals_implies_arrived in NTH_IN. Qed. End PeriodicLemmas.