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 module, we'll prove the known arrival times of jobs that stem from periodic tasks. *) Section PeriodicArrivalTimes. (** Consider periodic tasks with an offset ... *) Context {Task : TaskType}. Context `{TaskOffset Task}. Context `{PeriodicModel Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. (** Consider any unique arrival sequence with consistent arrivals ... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq. (** ... and any periodic task [tsk] with a valid offset and period. *) Variable tsk : Task. Hypothesis H_valid_offset: valid_offset arr_seq tsk. Hypothesis H_valid_period: valid_period tsk. Hypothesis H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk. (** We show that the nth job [j] of task [tsk] arrives at the instant [task_offset tsk + n * task_period tsk]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall (n : nat) (j : Job), arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j = task_offset tsk + n * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall (n : nat) (j : Job), arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j = task_offset tsk + n * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = 0 -> job_arrival j = task_offset tsk + 0 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j = task_offset tsk + n * task_period tsk
forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n.+1 -> job_arrival j = task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = 0 -> job_arrival j = task_offset tsk + 0 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
j: Job
ARR: arrives_in arr_seq j
TSK_IN: job_task j = tsk
ZINDEX: job_index arr_seq j = 0

job_arrival j = task_offset tsk + 0 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
j: Job
ARR: arrives_in arr_seq j
TSK_IN: job_task j = tsk
ZINDEX: job_index arr_seq j = 0

job_arrival j = task_offset tsk
exact: first_job_arrival ZINDEX.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j = task_offset tsk + n * task_period tsk

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n.+1 -> job_arrival j = task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j = task_offset tsk + n * task_period tsk

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n.+1 -> job_arrival j = task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j = task_offset tsk + n * task_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK_IN: job_task j = tsk
JB_INDEX: job_index arr_seq j = n.+1

job_arrival j = task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j = task_offset tsk + n * task_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK_IN: job_task j = tsk
JB_INDEX: job_index arr_seq j = n.+1
PREV_JOB: 0 < job_index arr_seq j -> job_task j = tsk -> exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk

job_arrival j = task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j = task_offset tsk + n * task_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK_IN: job_task j = tsk
JB_INDEX: job_index arr_seq j = n.+1
PREV_JOB: exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk

job_arrival j = task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j = task_offset tsk + n * task_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK_IN: job_task j = tsk
JB_INDEX: job_index arr_seq j = n.+1
pj: Job
ARR': arrives_in arr_seq pj
IND: job_index arr_seq pj = job_index arr_seq j - 1
TSK: job_task pj = tsk
ARRIVAL: job_arrival j = job_arrival pj + task_period tsk

job_arrival j = task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
pj: Job
IHn: job_arrival pj = task_offset tsk + n * task_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK_IN: job_task j = tsk
JB_INDEX: job_index arr_seq j = n.+1
ARR': arrives_in arr_seq pj
IND: job_index arr_seq pj = job_index arr_seq j - 1
TSK: job_task pj = tsk
ARRIVAL: job_arrival j = job_arrival pj + task_period tsk

job_arrival j = task_offset tsk + n.+1 * task_period tsk
rewrite ARRIVAL IHn; lia. } Qed. (** We show that for every job [j] of task [tsk] there exists a number [n] such that [j] arrives at the instant [task_offset tsk + n * task_period tsk]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> exists n : nat, job_arrival j = task_offset tsk + n * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> exists n : nat, job_arrival j = task_offset tsk + n * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

exists n : nat, job_arrival j = task_offset tsk + n * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

job_arrival j = task_offset tsk + job_index arr_seq j * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
J_ARR: arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = job_index arr_seq j -> job_arrival j = task_offset tsk + job_index arr_seq j * task_period tsk

job_arrival j = task_offset tsk + job_index arr_seq j * task_period tsk
by feed_n 3 J_ARR => //. Qed. (** If a job [j] of task [tsk] arrives at [task_offset tsk + n * task_period tsk] then the [job_index] of [j] is equal to [n]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall (n : nat) (j : Job), arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall (n : nat) (j : Job), arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk

forall (n : nat) (j : Job), arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + 0 * task_period tsk -> job_index arr_seq j = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n.+1 * task_period tsk -> job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + 0 * task_period tsk -> job_index arr_seq j = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n.+1 * task_period tsk -> job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk
j: Job
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + 0 * task_period tsk

job_index arr_seq j = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n.+1 * task_period tsk -> job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk
j: Job
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + 0 * task_period tsk
m: nat
SUCC: job_index arr_seq j = m.+1

job_index arr_seq j = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n.+1 * task_period tsk -> job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n.+1 * task_period tsk -> job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n

forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n.+1 * task_period tsk -> job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
j: Job
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk

job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: 0 < job_index arr_seq j -> job_task j = tsk -> exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk

0 < job_index arr_seq j
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk
job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: 0 < job_index arr_seq j -> job_task j = tsk -> exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk

0 < job_index arr_seq j
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: 0 < job_index arr_seq j -> job_task j = tsk -> exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk
EQ: job_index arr_seq j = 0

False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: 0 < job_index arr_seq j -> job_task j = tsk -> exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk
EQ: job_arrival j = task_offset tsk

False
by rewrite EQ in ARR; lia.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk

job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
IHn: forall j : Job, arrives_in arr_seq j -> job_task j = tsk -> job_arrival j = task_offset tsk + n * task_period tsk -> job_index arr_seq j = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRIVAL': job_arrival j = job_arrival j' + task_period tsk

job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
j': Job
IHn: job_index arr_seq j' = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRIVAL': job_arrival j = job_arrival j' + task_period tsk

job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
j': Job
IHn: job_index arr_seq j' = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk
ARR': arrives_in arr_seq j'
TSK': job_task j' = tsk
ARRIVAL': job_arrival j = job_arrival j' + task_period tsk
IND': n = job_index arr_seq j - 1

job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
j': Job
IHn: job_index arr_seq j' = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR: job_arrival j = task_offset tsk + n.+1 * task_period tsk
ARR': arrives_in arr_seq j'
TSK': job_task j' = tsk
ARRIVAL': job_arrival j = job_arrival j' + task_period tsk
IND': n = job_index arr_seq j - 1
Z: job_index arr_seq j = 0

job_index arr_seq j = n.+1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
j: Job
H_task_respects_periodic_model: exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
F: 0 < task_period tsk
n: nat
j': Job
IHn: job_index arr_seq j' = n
ARR_J: arrives_in arr_seq j
TSK: job_task j = tsk
ARR': arrives_in arr_seq j'
TSK': job_task j' = tsk
ARRIVAL': job_arrival j = job_arrival j' + task_period tsk
IND': n = job_index arr_seq j - 1
Z: job_index arr_seq j = 0
ARR: task_offset tsk = task_offset tsk + n.+1 * task_period tsk

job_index arr_seq j = n.+1
by lia. Qed. End PeriodicArrivalTimes.