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 properties concerning the size of task arrivals in context of the periodic model. *) Section TaskArrivalsSize. (** Consider any type of periodic tasks with an offset ... *) Context {Task : TaskType}. Context `{TaskOffset Task}. Context `{PeriodicModel Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. (** Consider any unique arrival sequence with consistent arrivals ... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq. (** ... and any periodic task [tsk] with a valid offset and period. *) Variable tsk : Task. Hypothesis H_valid_offset : valid_offset arr_seq tsk. Hypothesis H_valid_period : valid_period tsk. Hypothesis H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk. (** We show that if an instant [t] is not an "arrival time" for task [tsk] then [task_arrivals_at arr_seq tsk t] is an empty sequence. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall t : nat, (forall n : nat, t <> task_offset tsk + n * task_period tsk) -> task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall t : nat, (forall n : nat, t <> task_offset tsk + n * task_period tsk) -> task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk

task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk

forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk

forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk
t0: eqType
xs: seq t0

xs = [::] \/ (exists a : t0, a \in xs)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk
t0: eqType
a: t0
xs: seq t0
IHxs: xs = [::] \/ (exists a : t0, a \in xs)

a :: xs = [::] \/ (exists a0 : t0, a0 \in a :: xs)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk
t0: eqType
a: t0
xs: seq t0
IHxs: xs = [::] \/ (exists a : t0, a \in xs)

a \in a :: xs
by apply mem_head.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)

task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
A_IN: a \in task_arrivals_at arr_seq tsk t

task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
A_ARR: a \in arrivals_at arr_seq t

task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
A_ARR: a \in arrivals_at arr_seq t
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq

task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
T: forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
A_ARR: a \in arrivals_at arr_seq t
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t

task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR: a \in arr_seq t

task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR: arrives_in arr_seq a

task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR: arrives_in arr_seq a

exists n : nat, job_arrival a = 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
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR: arrives_in arr_seq a
EXISTS_N: exists n : nat, job_arrival a = task_offset tsk + n * task_period tsk
task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR: arrives_in arr_seq a
EXISTS_N: exists n : nat, job_arrival a = task_offset tsk + n * task_period tsk

task_arrivals_at arr_seq tsk t = [::]
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: nat
EMPT_OR_EXISTS: forall (t : eqType) (xs : seq t), xs = [::] \/ (exists a : t, a \in xs)
a: Job
TSK: job_task a = tsk
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
A_IN: job_arrival a = t
T: forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR: arrives_in arr_seq a
n: nat
A_ARRIVAL: job_arrival a = task_offset tsk + n * task_period tsk

task_arrivals_at arr_seq tsk t = [::]
by move : (T n) => T1. Qed. (** We show that at any instant [t], at most one job of task [tsk] can arrive (i.e. size of [task_arrivals_at arr_seq tsk t] is at most one). *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall t : instant, size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall t : instant, size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
LT: size (task_arrivals_at arr_seq tsk t) < 1

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
EXISTS_TWO: 1 < size (task_arrivals_at arr_seq tsk t) -> uniq (task_arrivals_at arr_seq tsk t) -> exists a b : Job, a <> b /\ a \in task_arrivals_at arr_seq tsk t /\ b \in task_arrivals_at arr_seq tsk t

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
EXISTS_TWO: 1 < size (task_arrivals_at arr_seq tsk t) -> uniq (task_arrivals_at arr_seq tsk t) -> exists a b : Job, a <> b /\ a \in task_arrivals_at arr_seq tsk t /\ b \in task_arrivals_at arr_seq tsk t
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
A_IN: a \in task_arrivals_at arr_seq tsk t
B_IN: b \in task_arrivals_at arr_seq tsk t

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
A_IN: job_of_task tsk a && (a \in arrivals_at arr_seq t)
B_IN: job_of_task tsk b && (b \in arrivals_at arr_seq t)

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: b \in arr_seq t
B_IN: a \in arr_seq t

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
SPO: respects_sporadic_task_model arr_seq tsk

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
SPO: respects_sporadic_task_model arr_seq tsk
EQ_ARR_A: job_arrival a = t

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
SPO: respects_sporadic_task_model arr_seq tsk
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
SPO: job_arrival a + task_min_inter_arrival_time tsk <= job_arrival b
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t
SPO: t + task_min_inter_arrival_time tsk <= t

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t
SPO: t + task_period tsk <= t

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
t: instant
GT: 1 < size (task_arrivals_at arr_seq tsk t)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = tsk
ARRA: a \in arrivals_at arr_seq t
TSKB: job_task b = tsk
ARRB: b \in arrivals_at arr_seq t
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
EQ_ARR_A: job_arrival a = t
EQ_ARR_B: job_arrival b = t
SPO: t + task_period tsk <= t
POS: 0 < task_period tsk

size (task_arrivals_at arr_seq tsk t) = 0 \/ size (task_arrivals_at arr_seq tsk t) = 1
by lia. Qed. (** We show that the size of task arrivals (strictly) between two consecutive arrival times is zero. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall n : nat, let l := (task_offset tsk + n * task_period tsk).+1 in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_between arr_seq tsk l r) = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk

forall n : nat, let l := (task_offset tsk + n * task_period tsk).+1 in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_between arr_seq tsk l r) = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat

size (task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk)) = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t: nat
INEQ: task_offset tsk + n * task_period tsk < t < task_offset tsk + n.+1 * task_period tsk

size (task_arrivals_at arr_seq tsk t) = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t: nat
INEQ: task_offset tsk + n * task_period tsk < t < task_offset tsk + n.+1 * task_period tsk
n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk

False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t, n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk
INEQ: task_offset tsk + n * task_period tsk < task_offset tsk + n1 * task_period tsk < task_offset tsk + n.+1 * task_period tsk

False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t, n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk
INEQ1: task_offset tsk + n * task_period tsk < task_offset tsk + n1 * task_period tsk
INEQ2: task_offset tsk + n1 * task_period tsk < task_offset tsk + n.+1 * task_period tsk

False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t, n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk
INEQ1: (0 < task_period tsk) && (n < n1)
INEQ2: (0 < task_period tsk) && (n1 < n.+1)

False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
n: nat
l:= (task_offset tsk + n * task_period tsk).+1: nat
r:= task_offset tsk + n.+1 * task_period tsk: nat
t, n1: nat
EQ: t = task_offset tsk + n1 * task_period tsk
A: 0 < task_period tsk
B: n < n1
C: 0 < task_period tsk
D: n1 < n.+1

False
by lia. Qed. (** In this section we show some properties of task arrivals in case of an infinite sequence of jobs. *) Section TaskArrivalsInCaseOfInfiniteJobs. (** Assume that we have an infinite sequence of jobs. *) Hypothesis H_infinite_jobs : infinite_jobs arr_seq. (** We show that for any number [n], there exists a job [j] of task [tsk] such that [job_index] of [j] is equal to [n] and [j] arrives at [task_offset tsk + n * task_period tsk]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

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

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

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

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

job_arrival j = task_offset tsk + n * task_period tsk
exact: (periodic_arrival_times arr_seq). Qed. (** We show that the size of task arrivals at any arrival time is equal to one. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

forall n : nat, let l := task_offset tsk + n * task_period tsk in size (task_arrivals_at arr_seq tsk l) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

forall n : nat, let l := task_offset tsk + n * task_period tsk in size (task_arrivals_at arr_seq tsk l) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
l:= task_offset tsk + n * task_period tsk: nat

size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
l:= task_offset tsk + n * task_period tsk: nat
j': Job
ARR: arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk + n * task_period tsk
IND: job_index arr_seq j' = n

size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
l:= task_offset tsk + n * task_period tsk: nat
j': Job
ARR: task_arrivals_at_job_arrival arr_seq j' = [:: j']
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk + n * task_period tsk
IND: job_index arr_seq j' = n

size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
l:= task_offset tsk + n * task_period tsk: nat
j': Job
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk + n * task_period tsk
IND: job_index arr_seq j' = n
ARR: task_arrivals_at arr_seq tsk (job_arrival j') = [:: j']

size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) = 1
by rewrite -ARRIVAL ARR. Qed. (** We show that the size of task arrivals up to [task_offset tsk] is equal to one. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

size (task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: 0 <= task_offset tsk -> task_offset tsk <= (task_offset tsk).+1 -> task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1

size (task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1

size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) + size (task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1

size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1
Z: size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) + size (task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1

size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1
t: nat
T_EQ: 0 <= t < task_offset tsk

size (task_arrivals_at arr_seq tsk t) = 0
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1
t: nat
T_EQ: 0 <= t < task_offset tsk
n: nat
EQ: t = task_offset tsk + n * task_period tsk

False
by lia.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1
Z: size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0

size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) + size (task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1
Z: size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0

size [seq j <- arrivals_at arr_seq (task_offset tsk) | job_of_task tsk j] = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
CAT: task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 = task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1
Z: size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
AT_SIZE: let l := task_offset tsk + 0 * task_period tsk in size (task_arrivals_at arr_seq tsk l) = 1

size [seq j <- arrivals_at arr_seq (task_offset tsk) | job_of_task tsk j] = 1
by rewrite mul0n addn0 in AT_SIZE. Qed. (** We show that for any number [n], the number of jobs released by task [tsk] up to [task_offset tsk + n * task_period tsk] is equal to [n + 1]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

forall n : nat, let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

forall n : nat, let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

let l := task_offset tsk + 0 * task_period tsk in let r := task_offset tsk + 1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = 0 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
let l := task_offset tsk + n.+1 * task_period tsk in let r := task_offset tsk + n.+2 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
l:= task_offset tsk + 0 * task_period tsk: nat
r:= task_offset tsk + 1 * task_period tsk: nat

size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
let l := task_offset tsk + n.+1 * task_period tsk in let r := task_offset tsk + n.+2 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1

let l := task_offset tsk + n.+1 * task_period tsk in let r := task_offset tsk + n.+2 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat

size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_offset tsk + n * task_period tsk <= task_offset tsk + n.+1 * task_period tsk -> task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1

size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1

size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1

n + 1 + size (task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_offset tsk + n * task_period tsk < task_offset tsk + n.+1 * task_period tsk -> task_offset tsk + n.+1 * task_period tsk <= (task_offset tsk + n.+1 * task_period tsk).+1 -> task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1 = task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1

n + 1 + size (task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_offset tsk + n * task_period tsk < task_offset tsk + n.+1 * task_period tsk -> task_offset tsk + n.+1 * task_period tsk <= (task_offset tsk + n.+1 * task_period tsk).+1 -> task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1 = task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1

task_offset tsk + n * task_period tsk < task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1 = task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1
n + 1 + size (task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_offset tsk + n * task_period tsk < task_offset tsk + n.+1 * task_period tsk -> task_offset tsk + n.+1 * task_period tsk <= (task_offset tsk + n.+1 * task_period tsk).+1 -> task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1 = task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1

task_offset tsk + n * task_period tsk < task_offset tsk + n.+1 * task_period tsk
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_offset tsk + n * task_period tsk < task_offset tsk + n.+1 * task_period tsk -> task_offset tsk + n.+1 * task_period tsk <= (task_offset tsk + n.+1 * task_period tsk).+1 -> task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1 = task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1

(0 < task_period tsk) && (n < n.+1)
by apply /andP; split => //.
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1 = task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1

n + 1 + size (task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1 = task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1

n + 1 + (size [seq j <- \cat_((task_offset tsk + n * task_period tsk).+1<=t<task_offset tsk + n.+1 * task_period tsk) arrivals_at arr_seq t | job_of_task tsk j] + size [seq j <- arrivals_at arr_seq (task_offset tsk + n.+1 * task_period tsk) | job_of_task tsk j]) = n.+1 + 1
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n: nat
IHn: let l := task_offset tsk + n * task_period tsk in let r := task_offset tsk + n.+1 * task_period tsk in size (task_arrivals_up_to arr_seq tsk l) = n + 1
l:= task_offset tsk + n.+1 * task_period tsk: nat
r:= task_offset tsk + n.+2 * task_period tsk: nat
CAT: task_arrivals_up_to arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) = task_arrivals_up_to arr_seq tsk (task_offset tsk + n * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1
S_CAT: task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk).+1 = task_arrivals_between arr_seq tsk (task_offset tsk + n * task_period tsk).+1 (task_offset tsk + n.+1 * task_period tsk) ++ task_arrivals_between arr_seq tsk (task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1

n + 1 + (0 + 1) = n.+1 + 1
by lia. Qed. (** We show that the number of jobs released by task [tsk] at any instant [t] and [t + n * task_period tsk] is the same for any number [n]. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

forall n t : nat, task_offset tsk <= t -> size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq

forall n t : nat, task_offset tsk <= t -> size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t

size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_eq0: (t - task_offset tsk) %% task_period tsk = 0

size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0
size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_eq0: (t - task_offset tsk) %% task_period tsk = 0

size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0
size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_eq0: (t - task_offset tsk) %% task_period tsk = 0

size (task_arrivals_at arr_seq tsk (task_offset tsk + ((t - task_offset tsk) %/ task_period tsk * task_period tsk + (t - task_offset tsk) %% task_period tsk))) = size (task_arrivals_at arr_seq tsk (task_offset tsk + ((t - task_offset tsk) %/ task_period tsk * task_period tsk + (t - task_offset tsk) %% task_period tsk) + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0
size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0

size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0

size (task_arrivals_at arr_seq tsk t) = size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0
n': nat

t + n * task_period tsk - task_offset tsk = n' * task_period tsk %[mod task_period tsk] -> False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0
n': nat
t - task_offset tsk = n' * task_period tsk %[mod task_period tsk] -> False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0
n': nat

t + n * task_period tsk - task_offset tsk = n' * task_period tsk %[mod task_period tsk] -> False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0
n': nat
t - task_offset tsk = n' * task_period tsk %[mod task_period tsk] -> False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0
n': nat

t - task_offset tsk = n' * task_period tsk %[mod task_period tsk] -> False
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_valid_offset: valid_offset arr_seq tsk
H_valid_period: valid_period tsk
H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk
H_infinite_jobs: infinite_jobs arr_seq
n, t: nat
o_le_t: task_offset tsk <= t
tmo_neq0: (t - task_offset tsk) %% task_period tsk <> 0
n': nat

t - task_offset tsk = n' * task_period tsk %[mod task_period tsk] -> False
by rewrite -[n' * _]addn0 modnMDl mod0n. Qed. End TaskArrivalsInCaseOfInfiniteJobs. End TaskArrivalsSize.