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 .
Require Export prosa.analysis.facts.periodic.arrival_times.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]
Require Export prosa.analysis.definitions.infinite_jobs.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]
Require Export prosa.analysis.facts.sporadic.arrival_sequence.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. *)
Lemma task_arrivals_size_at_non_arrival :
forall t ,
(forall n , t <> task_offset tsk + n * task_period tsk) ->
task_arrivals_at arr_seq tsk t = [::].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall t : nat,
(forall n : nat,
t <> task_offset tsk + n * task_period tsk) ->
task_arrivals_at arr_seq tsk t = [::]
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall t : nat,
(forall n : nat,
t <> task_offset tsk + n * task_period tsk) ->
task_arrivals_at arr_seq tsk t = [::]
intros * T.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat T : forall n : nat,
t <> task_offset tsk + n * task_period tsk
task_arrivals_at arr_seq tsk t = [::]
have EMPT_OR_EXISTS : forall xs , xs = [::] \/ exists a , a \in xs.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat T : forall n : nat,
t <> task_offset tsk + n * task_period tsk
forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
{ Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat T : forall n : nat,
t <> task_offset tsk + n * task_period tsk
forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
intros *.Task : TaskType H : TaskOffset Task H0 : PeriodicModel 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 tskt0 : eqType xs : seq t0
xs = [::] \/ (exists a : t0, a \in xs)
induction xs; first by left .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat T : forall n : nat,
t <> task_offset tsk + n * task_period tskt0 : eqType a : t0 xs : seq t0 IHxs : xs = [::] \/ (exists a : t0, a \in xs)
a :: xs = [::] \/ (exists a0 : t0, a0 \in a :: xs)
right ; exists a .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat T : forall n : nat,
t <> task_offset tsk + n * task_period tskt0 : 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 tskEMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
task_arrivals_at arr_seq tsk t = [::]
destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] => //.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat T : forall n : nat,
t <> task_offset tsk + n * task_period tskEMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)a : Job A_IN : a \in task_arrivals_at arr_seq tsk t
task_arrivals_at arr_seq tsk t = [::]
rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN => /andP [/eqP TSK A_ARR].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat T : forall n : nat,
t <> task_offset tsk + n * task_period tskEMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)a : Job TSK : job_task a = tsk A_ARR : a \in arrivals_at arr_seq t
task_arrivals_at arr_seq tsk t = [::]
move : H_valid_arrival_sequence => [CONSISTENT UNIQ].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat T : forall n : nat,
t <> task_offset tsk + n * task_period tskEMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)a : Job TSK : job_task a = tsk A_ARR : a \in arrivals_at arr_seq t CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq
task_arrivals_at arr_seq tsk t = [::]
move : (A_ARR) => A_IN; apply CONSISTENT in A_IN.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat T : forall n : nat,
t <> task_offset tsk + n * task_period tskEMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)a : Job TSK : job_task a = tsk A_ARR : a \in arrivals_at arr_seq t CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq A_IN : job_arrival a = t
task_arrivals_at arr_seq tsk t = [::]
rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)a : Job TSK : job_task a = tsk CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq A_IN : job_arrival a = t T : forall n : nat,
job_arrival a <>
task_offset tsk + n * task_period tskA_ARR : a \in arr_seq t
task_arrivals_at arr_seq tsk t = [::]
apply in_arrseq_implies_arrives in A_ARR.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)a : Job TSK : job_task a = tsk CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq A_IN : job_arrival a = t T : forall n : nat,
job_arrival a <>
task_offset tsk + n * task_period tskA_ARR : arrives_in arr_seq a
task_arrivals_at arr_seq tsk t = [::]
have EXISTS_N : exists n , job_arrival a = task_offset tsk + n * task_period tsk.Task : TaskType H : TaskOffset Task H0 : PeriodicModel 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 tskA_ARR : arrives_in arr_seq a
exists n : nat,
job_arrival a =
task_offset tsk + n * task_period tsk
exact : (job_arrival_times arr_seq).Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)a : Job TSK : job_task a = tsk CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq A_IN : job_arrival a = t T : forall n : nat,
job_arrival a <>
task_offset tsk + n * task_period tskA_ARR : arrives_in arr_seq a EXISTS_N : exists n : nat,
job_arrival a =
task_offset tsk + n * task_period tsk
task_arrivals_at arr_seq tsk t = [::]
move : EXISTS_N => [n A_ARRIVAL].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : nat EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)a : Job TSK : job_task a = tsk CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq A_IN : job_arrival a = t T : forall n : nat,
job_arrival a <>
task_offset tsk + n * task_period tskA_ARR : arrives_in arr_seq a n : nat A_ARRIVAL : job_arrival a =
task_offset tsk + n * task_period tsk
task_arrivals_at arr_seq tsk t = [::]
by move : (T n) => T1.
Qed .
(** We show that at any instant [t], at most one job of task [tsk]
can arrive (i.e. size of [task_arrivals_at arr_seq tsk t] is at most one). *)
Lemma task_arrivals_at_size_cases :
forall t ,
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1 .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall t : instant,
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall t : instant,
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
intro t.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
case : (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1 ) => [LT|GT|EQ]; try by auto .Task : TaskType H : TaskOffset Task H0 : PeriodicModel 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
destruct (size (task_arrivals_at arr_seq tsk t)); now left .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
specialize (exists_two (task_arrivals_at arr_seq tsk t)) => EXISTS_TWO.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)EXISTS_TWO : 1 < size (task_arrivals_at arr_seq tsk t) ->
uniq (task_arrivals_at arr_seq tsk t) ->
exists a b : Job,
a <> b /\
a \in task_arrivals_at arr_seq tsk t /\
b \in task_arrivals_at arr_seq tsk t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
move : H_valid_arrival_sequence => [CONSISTENT UNIQ].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)EXISTS_TWO : 1 < size (task_arrivals_at arr_seq tsk t) ->
uniq (task_arrivals_at arr_seq tsk t) ->
exists a b : Job,
a <> b /\
a \in task_arrivals_at arr_seq tsk t /\
b \in task_arrivals_at arr_seq tsk tCONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b A_IN : a \in task_arrivals_at arr_seq tsk t B_IN : b \in task_arrivals_at arr_seq tsk t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b A_IN : job_of_task tsk a &&
(a \in arrivals_at arr_seq t) B_IN : job_of_task tsk b &&
(b \in arrivals_at arr_seq t)
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
move : A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b TSKA : job_task a = tsk ARRA : a \in arrivals_at arr_seq t TSKB : job_task b = tsk ARRB : b \in arrivals_at arr_seq t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
move : (ARRA); move : (ARRB); rewrite /arrivals_at => A_IN B_IN.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b TSKA : job_task a = tsk ARRA : a \in arrivals_at arr_seq t TSKB : job_task b = tsk ARRB : b \in arrivals_at arr_seq t A_IN : b \in arr_seq t B_IN : a \in arr_seq t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b TSKA : job_task a = tsk ARRA : a \in arrivals_at arr_seq t TSKB : job_task b = tsk ARRB : b \in arrivals_at arr_seq t A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
have SPO : respects_sporadic_task_model arr_seq tsk; try by rt_auto.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b TSKA : job_task a = tsk ARRA : a \in arrivals_at arr_seq t TSKB : job_task b = tsk ARRB : b \in arrivals_at arr_seq t A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a SPO : respects_sporadic_task_model arr_seq tsk
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
have EQ_ARR_A : (job_arrival a = t) by rt_eauto.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b TSKA : job_task a = tsk ARRA : a \in arrivals_at arr_seq t TSKB : job_task b = tsk ARRB : b \in arrivals_at arr_seq t A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a SPO : respects_sporadic_task_model arr_seq tsk EQ_ARR_A : job_arrival a = t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
have EQ_ARR_B : (job_arrival b = t) by rt_eauto.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b TSKA : job_task a = tsk ARRA : a \in arrivals_at arr_seq t TSKB : job_task b = tsk ARRB : b \in arrivals_at arr_seq t A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a SPO : respects_sporadic_task_model arr_seq tsk EQ_ARR_A : job_arrival a = t EQ_ARR_B : job_arrival b = t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
specialize (SPO a b); feed_n 6 SPO => //; try by lia .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b TSKA : job_task a = tsk ARRA : a \in arrivals_at arr_seq t TSKB : job_task b = tsk ARRB : b \in arrivals_at arr_seq t A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a SPO : job_arrival a + task_min_inter_arrival_time tsk <=
job_arrival b EQ_ARR_A : job_arrival a = t EQ_ARR_B : job_arrival b = t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
rewrite EQ_ARR_A EQ_ARR_B in SPO.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b TSKA : job_task a = tsk ARRA : a \in arrivals_at arr_seq t TSKB : job_task b = tsk ARRB : b \in arrivals_at arr_seq t A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a EQ_ARR_A : job_arrival a = t EQ_ARR_B : job_arrival b = t SPO : t + task_min_inter_arrival_time tsk <= t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
rewrite /task_min_inter_arrival_time /periodic_as_sporadic in SPO.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk t : instant GT : 1 < size (task_arrivals_at arr_seq tsk t)CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq a, b : Job NEQ : a <> b TSKA : job_task a = tsk ARRA : a \in arrivals_at arr_seq t TSKB : job_task b = tsk ARRB : b \in arrivals_at arr_seq t A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a EQ_ARR_A : job_arrival a = t EQ_ARR_B : job_arrival b = t SPO : t + task_period tsk <= t
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
have POS : task_period tsk > 0 by auto .Task : TaskType H : TaskOffset Task H0 : PeriodicModel 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. *)
Lemma size_task_arrivals_between_eq0 :
forall n ,
let l := (task_offset tsk + n * task_period tsk).+1 in
let r := (task_offset tsk + n.+1 * task_period tsk) in
size (task_arrivals_between arr_seq tsk l r) = 0 .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall n : nat,
let l := (task_offset tsk + n * task_period tsk).+1 in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_between arr_seq tsk l r) = 0
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall n : nat,
let l := (task_offset tsk + n * task_period tsk).+1 in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_between arr_seq tsk l r) = 0
intros n l r; rewrite /l /r.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat l := (task_offset tsk + n * task_period tsk).+1 : nat r := task_offset tsk + n.+1 * task_period tsk : nat
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk)) = 0
rewrite size_of_task_arrivals_between big_nat_eq0 => //; intros t INEQ.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat l := (task_offset tsk + n * task_period tsk).+1 : nat r := task_offset tsk + n.+1 * task_period tsk : nat t : nat INEQ : task_offset tsk + n * task_period tsk < t <
task_offset tsk + n.+1 * task_period tsk
size (task_arrivals_at arr_seq tsk t) = 0
rewrite task_arrivals_size_at_non_arrival => //; intros n1 EQ.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat l := (task_offset tsk + n * task_period tsk).+1 : nat r := task_offset tsk + n.+1 * task_period tsk : nat t : nat INEQ : task_offset tsk + n * task_period tsk < t <
task_offset tsk + n.+1 * task_period tsk n1 : nat EQ : t = task_offset tsk + n1 * task_period tsk
False
rewrite EQ in INEQ.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat l := (task_offset tsk + n * task_period tsk).+1 : nat r := task_offset tsk + n.+1 * task_period tsk : nat t, n1 : nat EQ : t = task_offset tsk + n1 * task_period tsk INEQ : task_offset tsk + n * task_period tsk <
task_offset tsk + n1 * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
False
move : INEQ => /andP [INEQ1 INEQ2].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat l := (task_offset tsk + n * task_period tsk).+1 : nat r := task_offset tsk + n.+1 * task_period tsk : nat t, n1 : nat EQ : t = task_offset tsk + n1 * task_period tsk INEQ1 : task_offset tsk + n * task_period tsk <
task_offset tsk + n1 * task_period tsk INEQ2 : task_offset tsk + n1 * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
False
rewrite ltn_add2l ltn_mul2r in INEQ1; rewrite ltn_add2l ltn_mul2r in INEQ2.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat l := (task_offset tsk + n * task_period tsk).+1 : nat r := task_offset tsk + n.+1 * task_period tsk : nat t, n1 : nat EQ : t = task_offset tsk + n1 * task_period tsk INEQ1 : (0 < task_period tsk) && (n < n1) INEQ2 : (0 < task_period tsk) && (n1 < n.+1 )
False
move : INEQ1 INEQ2 => /andP [A B] /andP [C D].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat l := (task_offset tsk + n * task_period tsk).+1 : nat r := task_offset tsk + n.+1 * task_period tsk : nat t, n1 : nat EQ : t = task_offset tsk + n1 * task_period tsk A : 0 < task_period tskB : n < n1 C : 0 < task_period tskD : n1 < n.+1
False
by lia .
Qed .
(** In this section we show some properties of task arrivals in case
of an infinite sequence of jobs. *)
Section TaskArrivalsInCaseOfInfiniteJobs .
(** Assume that we have an infinite sequence of jobs. *)
Hypothesis H_infinite_jobs : infinite_jobs arr_seq.
(** We show that for any number [n], there exists a job [j] of task [tsk]
such that [job_index] of [j] is equal to [n] and [j] arrives
at [task_offset tsk + n * task_period tsk]. *)
Lemma jobs_exists_later :
forall n ,
exists j ,
arrives_in arr_seq j /\
job_task j = tsk /\
job_arrival j = task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
forall n : nat,
exists j : Job,
arrives_in arr_seq j /\
job_task j = tsk /\
job_arrival j =
task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
forall n : nat,
exists j : Job,
arrives_in arr_seq j /\
job_task j = tsk /\
job_arrival j =
task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n
intros *.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat
exists j : Job,
arrives_in arr_seq j /\
job_task j = tsk /\
job_arrival j =
task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n
destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat j : Job ARR : arrives_in arr_seq j TSK : job_task j = tsk IND : job_index arr_seq j = n
exists j : Job,
arrives_in arr_seq j /\
job_task j = tsk /\
job_arrival j =
task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n
exists j ; repeat split => //.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat j : Job ARR : arrives_in arr_seq j TSK : job_task j = tsk IND : job_index arr_seq j = n
job_arrival j = task_offset tsk + n * task_period tsk
exact : (periodic_arrival_times arr_seq).
Qed .
(** We show that the size of task arrivals at any arrival time is equal to one. *)
Lemma task_arrivals_at_size :
forall n ,
let l := (task_offset tsk + n * task_period tsk) in
size (task_arrivals_at arr_seq tsk l) = 1 .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
intros n l; rewrite /l.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat l := task_offset tsk + n * task_period tsk : nat
size
(task_arrivals_at arr_seq tsk
(task_offset tsk + n * task_period tsk)) = 1
move : (jobs_exists_later n) => [j' [ARR [TSK [ARRIVAL IND]]]].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat l := task_offset tsk + n * task_period tsk : nat j' : Job ARR : arrives_in arr_seq j' TSK : job_task j' = tsk ARRIVAL : job_arrival j' =
task_offset tsk + n * task_period tsk IND : job_index arr_seq j' = n
size
(task_arrivals_at arr_seq tsk
(task_offset tsk + n * task_period tsk)) = 1
apply (only_j_in_task_arrivals_at_j
arr_seq H_valid_arrival_sequence tsk) in ARR => //;
last by rt_auto.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat l := task_offset tsk + n * task_period tsk : nat j' : Job ARR : task_arrivals_at_job_arrival arr_seq j' =
[:: j'] TSK : job_task j' = tsk ARRIVAL : job_arrival j' =
task_offset tsk + n * task_period tsk IND : job_index arr_seq j' = n
size
(task_arrivals_at arr_seq tsk
(task_offset tsk + n * task_period tsk)) = 1
rewrite /task_arrivals_at_job_arrival TSK in ARR.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat l := task_offset tsk + n * task_period tsk : nat j' : Job TSK : job_task j' = tsk ARRIVAL : job_arrival j' =
task_offset tsk + n * task_period tsk IND : job_index arr_seq j' = n ARR : task_arrivals_at arr_seq tsk (job_arrival j') =
[:: j']
size
(task_arrivals_at arr_seq tsk
(task_offset tsk + n * task_period tsk)) = 1
by rewrite -ARRIVAL ARR.
Qed .
(** We show that the size of task arrivals up to [task_offset tsk] is equal to one. *)
Lemma size_task_arrivals_up_to_offset :
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1 .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
size
(task_arrivals_up_to arr_seq tsk (task_offset tsk)) =
1
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
size
(task_arrivals_up_to arr_seq tsk (task_offset tsk)) =
1
rewrite /task_arrivals_up_to.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
size
(task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 ) = 1
specialize (task_arrivals_between_cat arr_seq tsk 0 (task_offset tsk) (task_offset tsk).+1 ) => CAT.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq CAT : 0 <= task_offset tsk ->
task_offset tsk <= (task_offset tsk).+1 ->
task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
(task_offset tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk)
(task_offset tsk).+1
size
(task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 ) = 1
feed_n 2 CAT => //; rewrite CAT size_cat. Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq CAT : task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
(task_offset tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk)
(task_offset tsk).+1
size
(task_arrivals_between arr_seq tsk 0
(task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1 ) = 1
have Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0 .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq CAT : task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
(task_offset tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk)
(task_offset tsk).+1
size
(task_arrivals_between arr_seq tsk 0
(task_offset tsk)) = 0
{ Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq CAT : task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
(task_offset tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk)
(task_offset tsk).+1
size
(task_arrivals_between arr_seq tsk 0
(task_offset tsk)) = 0
rewrite size_of_task_arrivals_between big_nat_eq0 => //; intros t T_EQ.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq CAT : task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
(task_offset tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk)
(task_offset tsk).+1 t : nat T_EQ : 0 <= t < task_offset tsk
size (task_arrivals_at arr_seq tsk t) = 0
rewrite task_arrivals_size_at_non_arrival => //; intros n EQ.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq CAT : task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
(task_offset tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk)
(task_offset tsk).+1 t : nat T_EQ : 0 <= t < task_offset tskn : nat EQ : t = task_offset tsk + n * task_period tsk
False
by lia .
} Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq CAT : task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
(task_offset tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk)
(task_offset tsk).+1 Z : size
(task_arrivals_between arr_seq tsk 0
(task_offset tsk)) = 0
size
(task_arrivals_between arr_seq tsk 0
(task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1 ) = 1
rewrite Z add0n /task_arrivals_between /arrivals_between big_nat1.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq CAT : task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
(task_offset tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk)
(task_offset tsk).+1 Z : size
(task_arrivals_between arr_seq tsk 0
(task_offset tsk)) = 0
size
[seq j <- arrivals_at arr_seq (task_offset tsk)
| job_of_task tsk j] = 1
specialize (task_arrivals_at_size 0 ) => AT_SIZE.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq CAT : task_arrivals_between arr_seq tsk 0
(task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0
(task_offset tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk)
(task_offset tsk).+1 Z : size
(task_arrivals_between arr_seq tsk 0
(task_offset tsk)) = 0 AT_SIZE : let l :=
task_offset tsk + 0 * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
size
[seq j <- arrivals_at arr_seq (task_offset tsk)
| job_of_task tsk j] = 1
by rewrite mul0n addn0 in AT_SIZE.
Qed .
(** We show that for any number [n], the number of jobs released by task [tsk] up to
[task_offset tsk + n * task_period tsk] is equal to [n + 1]. *)
Lemma task_arrivals_up_to_size :
forall n ,
let l := (task_offset tsk + n * task_period tsk) in
let r := (task_offset tsk + n.+1 * task_period tsk) in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
induction 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
let l := task_offset tsk + 0 * task_period tsk in
let r := task_offset tsk + 1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = 0 + 1
intros l r; rewrite /l mul0n add0n addn0.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq l := task_offset tsk + 0 * task_period tsk : nat r := task_offset tsk + 1 * task_period tsk : nat
size
(task_arrivals_up_to arr_seq tsk (task_offset tsk)) =
1
by apply size_task_arrivals_up_to_offset.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
let l := task_offset tsk + n.+1 * task_period tsk in
let r := task_offset tsk + n.+2 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
intros l r.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
specialize (task_arrivals_cat arr_seq tsk (task_offset tsk + n * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk)) => CAT.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_offset tsk + n * task_period tsk <=
task_offset tsk + n.+1 * task_period tsk ->
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
feed_n 1 CAT; first by lia . Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
rewrite CAT size_cat IHn.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 ) =
n.+1 + 1
specialize (task_arrivals_between_cat arr_seq tsk (task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1 ) => S_CAT.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 ) =
n.+1 + 1
feed_n 2 S_CAT; try by lia . Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
{ Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
rewrite ltn_add2l ltn_mul2r.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
(0 < task_period tsk) && (n < n.+1 )
by apply /andP; split => //.
} Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 S_CAT : task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 ) =
n.+1 + 1
rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 S_CAT : task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
n + 1 +
(size
[seq j <- \cat_((task_offset tsk +
n * task_period tsk).+1 <=t<task_offset
tsk +
n.+1 *
task_period
tsk)
arrivals_at arr_seq t
| job_of_task tsk j] +
size
[seq j <- arrivals_at arr_seq
(task_offset tsk +
n.+1 * task_period tsk)
| job_of_task tsk j]) = n.+1 + 1
rewrite size_task_arrivals_between_eq0 task_arrivals_at_size => //.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n : nat IHn : let l := task_offset tsk + n * task_period tsk
in
let r :=
task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1 l := task_offset tsk + n.+1 * task_period tsk : nat r := task_offset tsk + n.+2 * task_period tsk : nat CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 S_CAT : task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
n + 1 + (0 + 1 ) = n.+1 + 1
by lia .
Qed .
(** We show that the number of jobs released by task [tsk] at any instant [t]
and [t + n * task_period tsk] is the same for any number [n]. *)
Lemma eq_size_of_task_arrivals_seperated_by_period :
forall n t ,
t >= task_offset tsk ->
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk)).Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
forall n t : nat,
task_offset tsk <= t ->
size (task_arrivals_at arr_seq tsk t) =
size
(task_arrivals_at arr_seq tsk
(t + n * task_period tsk))
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq
forall n t : nat,
task_offset tsk <= t ->
size (task_arrivals_at arr_seq tsk t) =
size
(task_arrivals_at arr_seq tsk
(t + n * task_period tsk))
move => n t o_le_t.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n, t : nat o_le_t : task_offset tsk <= t
size (task_arrivals_at arr_seq tsk t) =
size
(task_arrivals_at arr_seq tsk
(t + n * task_period tsk))
have [tmo_eq0|tmo_neq0] :=
@eqP _ ((t - task_offset tsk) %% task_period tsk) 0 .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n, t : nat o_le_t : task_offset tsk <= t tmo_eq0 : (t - task_offset tsk) %% task_period tsk = 0
size (task_arrivals_at arr_seq tsk t) =
size
(task_arrivals_at arr_seq tsk
(t + n * task_period tsk))
- Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n, t : nat o_le_t : task_offset tsk <= t tmo_eq0 : (t - task_offset tsk) %% task_period tsk = 0
size (task_arrivals_at arr_seq tsk t) =
size
(task_arrivals_at arr_seq tsk
(t + n * task_period tsk))
rewrite -(subnKC o_le_t) (divn_eq (t - _) (task_period tsk)).Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n, t : nat o_le_t : task_offset tsk <= t tmo_eq0 : (t - task_offset tsk) %% task_period tsk = 0
size
(task_arrivals_at arr_seq tsk
(task_offset tsk +
((t - task_offset tsk) %/ task_period tsk *
task_period tsk +
(t - task_offset tsk) %% task_period tsk))) =
size
(task_arrivals_at arr_seq tsk
(task_offset tsk +
((t - task_offset tsk) %/ task_period tsk *
task_period tsk +
(t - task_offset tsk) %% task_period tsk) +
n * task_period tsk))
by rewrite tmo_eq0 addn0 -addnA -mulnDl !task_arrivals_at_size.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n, t : nat o_le_t : task_offset tsk <= t tmo_neq0 : (t - task_offset tsk) %% task_period tsk <>
0
size (task_arrivals_at arr_seq tsk t) =
size
(task_arrivals_at arr_seq tsk
(t + n * task_period tsk))
- Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n, t : nat o_le_t : task_offset tsk <= t tmo_neq0 : (t - task_offset tsk) %% task_period tsk <>
0
size (task_arrivals_at arr_seq tsk t) =
size
(task_arrivals_at arr_seq tsk
(t + n * task_period tsk))
rewrite !task_arrivals_size_at_non_arrival// => n';
move => /(f_equal (subn^~(task_offset tsk))); rewrite addKn;
move => /(f_equal (modn^~(task_period tsk))).Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n, t : nat o_le_t : task_offset tsk <= t tmo_neq0 : (t - task_offset tsk) %% task_period tsk <>
0 n' : nat
t + n * task_period tsk - task_offset tsk
= n' * task_period tsk
%[mod task_period tsk] -> False
+ Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n, t : nat o_le_t : task_offset tsk <= t tmo_neq0 : (t - task_offset tsk) %% task_period tsk <>
0 n' : nat
t + n * task_period tsk - task_offset tsk
= n' * task_period tsk
%[mod task_period tsk] -> False
by rewrite -addnBAC// addnC -[n' * _]addn0 !modnMDl mod0n.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk H_infinite_jobs : infinite_jobs arr_seq n, t : nat o_le_t : task_offset tsk <= t tmo_neq0 : (t - task_offset tsk) %% task_period tsk <>
0 n' : nat
t - task_offset tsk
= n' * task_period tsk
%[mod task_period tsk] -> False
+ Task : TaskType H : TaskOffset Task H0 : PeriodicModel 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 .