Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.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.definitions.delay_propagation.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.behavior.arrivals.
(** * Propagation of Delays in Arrival Curves *)
(** In this module, we prove properties of the generic delay propagation
definitions provided in [prosa.analysis.definitions.delay_propagation]. *)
Section ACPropFacts .
(** Consider two kinds of tasks... *)
Context {Task1 Task2 : TaskType}.
(** ... and their associated kinds of jobs. *)
Context {Job1 Job2 : JobType}
`{JobTask Job1 Task1} `{JobTask Job2 Task2}
(JA1 : JobArrival Job1) (JA2 : JobArrival Job2).
(** Suppose we are given a mapping of jobs (resp., tasks) of the second kind
to jobs (resp., tasks) of the first kind. *)
Variable job1_of : Job2 -> Job1.
Variable task1_of : Task2 -> Task1.
(** Furthermore, suppose we also have a reverse mapping from jobs of the first
kind to the associated jobs of the second kind. *)
Variable job2_of : Job1 -> seq Job2.
(** The relation of the jobs is as follows: a job [j2 : Job2] arrives exactly
[arrival_delay j2] time units after the arrival of its corresponding job
[job1_of j2], where the maximum possible delay is bounded by [delay_bound
(job_task j2)]. *)
Variable arrival_delay : Job2 -> duration.
Variable delay_bound : Task2 -> duration.
(** Consider any set of type-two tasks. *)
Variable ts2 : seq Task2.
(** If the mapping of type-two tasks to type-one tasks is valid for the tasks
in the considered task set, ... *)
Hypothesis H_valid_mapping :
valid_delay_propagation_mapping
JA1 JA2 job1_of task1_of delay_bound ts2.
(** ... and we are given an arrival curve for the first kind of tasks, ... *)
Context {max_arrivals1 : MaxArrivals Task1}.
(** ... then we obtain a derived (or propagated) arrival curve for tasks of
the second kind. *)
#[local] Instance max_arrivals2 : MaxArrivals Task2 :=
propagated_arrival_curve task1_of delay_bound.
(** Additionally, given an arbitrary arrival sequence of type-one jobs, *)
Variable arr_seq1 : arrival_sequence Job1.
(** ... if the mapping of type-two jobs to type-one jobs is valid, ... *)
Hypothesis H_arr_seq_mapping :
valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound arr_seq1 job2_of arrival_delay ts2.
(** ... it induces a derived arrival sequence of type-two jobs. *)
Let arr_seq2 := propagated_arrival_sequence JA1 job1_of arr_seq1 job2_of arrival_delay.
(** ** Arrival Sequence Validity Properties *)
(** In the following, we establish that the derived arrival sequence is
structurally valid. *)
(** First, the induced arrival sequence is consistent with the arrival times
of type-two jobs. *)
Lemma consistent_propagated_arrival_sequence :
consistent_arrival_times arr_seq2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
consistent_arrival_times arr_seq2
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
consistent_arrival_times arr_seq2
move => j2 t.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 t : instant
arrives_at arr_seq2 j2 t -> job_arrival j2 = t
rewrite /arrives_at/arrivals_at/arr_seq2/propagated_arrival_sequence.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 t : instant
j2
\in [seq j2 <- flatten
[seq job2_of j
| j <- arrivals_up_to arr_seq1 t]
| job_arrival (job1_of j2) + arrival_delay j2 ==
t] -> job_arrival j2 = t
rewrite mem_filter => /andP[/eqP <- _].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 t : instant
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2
by move : H_arr_seq_mapping => [_ _ _ {}].
Qed .
(** Second, the induced arrival sequence does not duplicate any jobs. *)
Lemma propagated_arrival_sequence_uniq :
valid_arrival_sequence arr_seq1 ->
arrival_sequence_uniq arr_seq2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
valid_arrival_sequence arr_seq1 ->
arrival_sequence_uniq arr_seq2
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
valid_arrival_sequence arr_seq1 ->
arrival_sequence_uniq arr_seq2
move => VALID t.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant
uniq (arrivals_at arr_seq2 t)
rewrite /arrivals_at/arr_seq2/propagated_arrival_sequence.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant
uniq
[seq j2 <- flatten
[seq job2_of j
| j <- arrivals_up_to arr_seq1 t]
| job_arrival (job1_of j2) + arrival_delay j2 ==
t]
apply : filter_uniq.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant
uniq
(flatten
[seq job2_of j | j <- arrivals_up_to arr_seq1 t])
rewrite /flatten foldrE big_map big_seq.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant
uniq
(\cat_(i<-arrivals_up_to arr_seq1 t|i
\in arrivals_up_to
arr_seq1
t)
job2_of i)
apply : bigcat_uniq.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant
forall x : Job1,
x \in arrivals_up_to arr_seq1 t -> uniq (job2_of x)
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant
forall x : Job1,
x \in arrivals_up_to arr_seq1 t -> uniq (job2_of x)
move => j1 IN.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant j1 : Job1 IN : j1 \in arrivals_up_to arr_seq1 t
uniq (job2_of j1)
move : H_arr_seq_mapping => [_ UNIQ _ _]; apply UNIQ.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant j1 : Job1 IN : j1 \in arrivals_up_to arr_seq1 t UNIQ : job_mapping_uniq arr_seq1 job2_of
arrives_in arr_seq1 j1
apply : in_arrivals_implies_arrived.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant j1 : Job1 IN : j1 \in arrivals_up_to arr_seq1 t UNIQ : job_mapping_uniq arr_seq1 job2_of
j1 \in arrivals_between arr_seq1 ?Goal1 ?Goal2
exact : IN.
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant
forall (x : Job2) (y z : Job1),
x \in job2_of y -> x \in job2_of z -> y = z
move => j2 j1 j1'.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant j2 : Job2 j1, j1' : Job1
j2 \in job2_of j1 -> j2 \in job2_of j1' -> j1 = j1'
move : H_arr_seq_mapping => [CON _ _ _].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant j2 : Job2 j1, j1' : Job1 CON : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1
j2 \in job2_of j1 -> j2 \in job2_of j1' -> j1 = j1'
by rewrite !CON => -> ->.
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 VALID : valid_arrival_sequence arr_seq1 t : instant
uniq (arrivals_up_to arr_seq1 t)
by apply : arrivals_uniq.
Qed .
(** Taken together, the above two lemmas imply that the derived arrival
sequence is valid if the reference arrival sequence is valid. *)
Corollary valid_propagated_arrival_sequence :
valid_arrival_sequence arr_seq1 ->
valid_arrival_sequence arr_seq2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
valid_arrival_sequence arr_seq1 ->
valid_arrival_sequence arr_seq2
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
valid_arrival_sequence arr_seq1 ->
valid_arrival_sequence arr_seq2
split ; first exact : consistent_propagated_arrival_sequence.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 H1 : valid_arrival_sequence arr_seq1
arrival_sequence_uniq arr_seq2
exact : propagated_arrival_sequence_uniq.
Qed .
(** A job of the second kind [j2 : Job2] is part of the derived arrival
sequence if its associated job of the first kind [job1_of j2] is part of
the given reference arrival sequence. *)
Lemma arrives_in_propagated_if :
forall j2 ,
consistent_arrival_times arr_seq1 ->
arrives_in arr_seq1 (job1_of j2) -> arrives_in arr_seq2 j2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
forall j2 : Job2,
consistent_arrival_times arr_seq1 ->
arrives_in arr_seq1 (job1_of j2) ->
arrives_in arr_seq2 j2
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
forall j2 : Job2,
consistent_arrival_times arr_seq1 ->
arrives_in arr_seq1 (job1_of j2) ->
arrives_in arr_seq2 j2
move => j2 CAT1 IN; move : (IN) => [t IN'].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 CAT1 : consistent_arrival_times arr_seq1 IN : arrives_in arr_seq1 (job1_of j2) t : instant IN' : job1_of j2 \in arrivals_at arr_seq1 t
arrives_in arr_seq2 j2
exists (t + arrival_delay j2).Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 CAT1 : consistent_arrival_times arr_seq1 IN : arrives_in arr_seq1 (job1_of j2) t : instant IN' : job1_of j2 \in arrivals_at arr_seq1 t
j2 \in arrivals_at arr_seq2 (t + arrival_delay j2)
rewrite /arrivals_at/arr_seq2/propagated_arrival_sequence.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 CAT1 : consistent_arrival_times arr_seq1 IN : arrives_in arr_seq1 (job1_of j2) t : instant IN' : job1_of j2 \in arrivals_at arr_seq1 t
j2
\in [seq j3 <- flatten
[seq job2_of j
| j <- arrivals_up_to arr_seq1
(t + arrival_delay j2)]
| job_arrival (job1_of j3) + arrival_delay j3 ==
t + arrival_delay j2]
rewrite mem_filter; apply /andP; split ;
first by rewrite (CAT1 _ t).Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 CAT1 : consistent_arrival_times arr_seq1 IN : arrives_in arr_seq1 (job1_of j2) t : instant IN' : job1_of j2 \in arrivals_at arr_seq1 t
j2
\in flatten
[seq job2_of j
| j <- arrivals_up_to arr_seq1
(t + arrival_delay j2)]
apply /flatten_mapP.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 CAT1 : consistent_arrival_times arr_seq1 IN : arrives_in arr_seq1 (job1_of j2) t : instant IN' : job1_of j2 \in arrivals_at arr_seq1 t
exists2 x : Job1,
x \in arrivals_up_to arr_seq1 (t + arrival_delay j2) &
j2 \in job2_of x
exists (job1_of j2 ).Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 CAT1 : consistent_arrival_times arr_seq1 IN : arrives_in arr_seq1 (job1_of j2) t : instant IN' : job1_of j2 \in arrivals_at arr_seq1 t
job1_of j2
\in arrivals_up_to arr_seq1 (t + arrival_delay j2)
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 CAT1 : consistent_arrival_times arr_seq1 IN : arrives_in arr_seq1 (job1_of j2) t : instant IN' : job1_of j2 \in arrivals_at arr_seq1 t
job1_of j2
\in arrivals_up_to arr_seq1 (t + arrival_delay j2)
apply : job_in_arrivals_between => //.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 CAT1 : consistent_arrival_times arr_seq1 IN : arrives_in arr_seq1 (job1_of j2) t : instant IN' : job1_of j2 \in arrivals_at arr_seq1 t
job_arrival (job1_of j2) < (t + arrival_delay j2).+1
by rewrite (CAT1 _ t) //; lia .
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 CAT1 : consistent_arrival_times arr_seq1 IN : arrives_in arr_seq1 (job1_of j2) t : instant IN' : job1_of j2 \in arrivals_at arr_seq1 t
j2 \in job2_of (job1_of j2)
by move : H_arr_seq_mapping => [-> _].
Qed .
(** Conversely, a job of the second kind [j2 : Job2] is part of the derived
arrival sequence _only if_ its associated job of the first kind [job1_of
j2] is part of the given reference arrival sequence. *)
Lemma arrives_in_propagated_only_if :
forall j2 ,
arrives_in arr_seq2 j2 -> arrives_in arr_seq1 (job1_of j2).Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
forall j2 : Job2,
arrives_in arr_seq2 j2 ->
arrives_in arr_seq1 (job1_of j2)
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
forall j2 : Job2,
arrives_in arr_seq2 j2 ->
arrives_in arr_seq1 (job1_of j2)
move => j2 [t2 {}].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 t2 : instant
j2 \in arrivals_at arr_seq2 t2 ->
arrives_in arr_seq1 (job1_of j2)
rewrite /arrivals_at/arr_seq2/propagated_arrival_sequence.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 t2 : instant
j2
\in [seq j2 <- flatten
[seq job2_of j
| j <- arrivals_up_to arr_seq1
t2]
| job_arrival (job1_of j2) + arrival_delay j2 ==
t2] -> arrives_in arr_seq1 (job1_of j2)
rewrite mem_filter => /andP[/eqP DEF /flatten_mapP[j1 IN1 {}]].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 t2 : instant DEF : job_arrival (job1_of j2) + arrival_delay j2 = t2 j1 : Job1 IN1 : j1 \in arrivals_up_to arr_seq1 t2
j2 \in job2_of j1 -> arrives_in arr_seq1 (job1_of j2)
move : H_arr_seq_mapping => [-> _ _ _] ->.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 j2 : Job2 t2 : instant DEF : job_arrival (job1_of j2) + arrival_delay j2 = t2 j1 : Job1 IN1 : j1 \in arrivals_up_to arr_seq1 t2
arrives_in arr_seq1 j1
by apply /in_arrivals_implies_arrived/IN1.
Qed .
(** ** Correctness of the Propagated Arrival Curve *)
(** Next, we establish the correctness of the propagated arrival curve. *)
(** To this end, we first observe that the defined function satisfies the
structural requirements for arrival curves. *)
Lemma propagated_arrival_curve_valid :
(forall tsk2 , tsk2 \in ts2 -> monotone leq (@max_arrivals Task1 max_arrivals1 (task1_of tsk2))) ->
valid_taskset_arrival_curve ts2 max_arrivals2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
(forall tsk2 : Task2,
tsk2 \in ts2 ->
monotone leq (max_arrivals (task1_of tsk2))) ->
valid_taskset_arrival_curve ts2 max_arrivals2
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2
(forall tsk2 : Task2,
tsk2 \in ts2 ->
monotone leq (max_arrivals (task1_of tsk2))) ->
valid_taskset_arrival_curve ts2 max_arrivals2
move => MONO tsk2 IN2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 MONO : forall tsk2 : Task2,
tsk2 \in ts2 ->
monotone leq (max_arrivals (task1_of tsk2))tsk2 : Task2 IN2 : tsk2 \in ts2
valid_arrival_curve (max_arrivals2 tsk2)
split => // delta1 delta2 LEQ.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 MONO : forall tsk2 : Task2,
tsk2 \in ts2 ->
monotone leq (max_arrivals (task1_of tsk2))tsk2 : Task2 IN2 : tsk2 \in ts2 delta1, delta2 : nat LEQ : delta1 <= delta2
max_arrivals2 tsk2 delta1 <= max_arrivals2 tsk2 delta2
case : delta1 LEQ; case : delta2 => //= delta2 delta1 LEQ.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 MONO : forall tsk2 : Task2,
tsk2 \in ts2 ->
monotone leq (max_arrivals (task1_of tsk2))tsk2 : Task2 IN2 : tsk2 \in ts2 delta2, delta1 : nat LEQ : delta1 < delta2.+1
max_arrivals (task1_of tsk2)
(delta1.+1 + delay_bound tsk2) <=
max_arrivals (task1_of tsk2)
(delta2.+1 + delay_bound tsk2)
apply : MONO => //.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 tsk2 : Task2 IN2 : tsk2 \in ts2 delta2, delta1 : nat LEQ : delta1 < delta2.+1
delta1.+1 + delay_bound tsk2 <=
delta2.+1 + delay_bound tsk2
by lia .
Qed .
(** In the following, let [ts1] denote the set of type-one tasks that the
type-two tasks in [ts2] are mapped to (by [task1_of]). *)
Let ts1 := [seq task1_of tsk2 | tsk2 <- ts2].
(** To establish correctness, we make the assumption that each job of the
first kind has at most one associated job of the second kind.
Generalizations to multiple successors are possible, but the current
definition of [propagated_arrival_curve] works only under this
restriction. *)
Hypothesis H_job2_of_singleton :
(forall tsk1 ,
tsk1 \in ts1 -> forall j1 ,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 ).
(** Suppose the given type-one arrival sequence and arrival curve are
valid. *)
Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq1.
Hypothesis H_valid_ac : valid_taskset_arrival_curve ts1 max_arrivals1.
(** In preparation of the correctness argument, we next establish a couple of
"stepping stone" lemmas that sketch the main thrust of the correctness
argument. *)
Section ArrivalCurveCorrectnessSteps .
(** Consider an interval <<[t1, t2)>> ... *)
Variable t1 t2 : instant.
Hypothesis H_ordered : t1 <= t2.
(** ... and any type-two task in the given task set. *)
Variable tsk2 : Task2.
Hypothesis H_in_ts : tsk2 \in ts2.
(** Let [tsk2_arrivals] denote the jobs of [tsk2] that arrive in the
interval <<[t1, t2)>> ... *)
Let tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1 t2.
(** ... and let [trigger_jobs] denote the corresponding type-one jobs. *)
Let trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals].
(** First, note that the arrival times of the jobs in [trigger_jobs]
necessarily fall into the window <<[t1 - delay_bound tsk2, t2)>>. *)
Lemma trigger_job_arrival_bounded :
forall j1 ,
j1 \in trigger_jobs ->
(t1 - delay_bound tsk2) <= job_arrival j1 < t2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1
forall j1 : Job1,
j1 \in trigger_jobs ->
t1 - delay_bound tsk2 <= job_arrival j1 < t2
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1
forall j1 : Job1,
j1 \in trigger_jobs ->
t1 - delay_bound tsk2 <= job_arrival j1 < t2
move : H_arr_seq_mapping => [_ _ BOUND DEF].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 BOUND : forall j2 : Job2,
job_task j2 \in ts2 ->
arrives_in arr_seq1 (job1_of j2) ->
arrival_delay j2 <= delay_bound (job_task j2)DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2
forall j1 : Job1,
j1 \in trigger_jobs ->
t1 - delay_bound tsk2 <= job_arrival j1 < t2
move => j1 /mapP [j2] /[!mem_filter] /andP [SRC2 ARR2] EQ.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 BOUND : forall j2 : Job2,
job_task j2 \in ts2 ->
arrives_in arr_seq1 (job1_of j2) ->
arrival_delay j2 <= delay_bound (job_task j2)DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 SRC2 : job_of_task tsk2 j2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2
t1 - delay_bound tsk2 <= job_arrival j1 < t2
move : SRC2; rewrite /job_of_task => /eqP SRC2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 BOUND : forall j2 : Job2,
job_task j2 \in ts2 ->
arrives_in arr_seq1 (job1_of j2) ->
arrival_delay j2 <= delay_bound (job_task j2)DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2
t1 - delay_bound tsk2 <= job_arrival j1 < t2
have /andP[j2t1 j2t2]: t1 <= job_arrival j2 < t2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 BOUND : forall j2 : Job2,
job_task j2 \in ts2 ->
arrives_in arr_seq1 (job1_of j2) ->
arrival_delay j2 <= delay_bound (job_task j2)DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2
t1 <= job_arrival j2 < t2
{ Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 BOUND : forall j2 : Job2,
job_task j2 \in ts2 ->
arrives_in arr_seq1 (job1_of j2) ->
arrival_delay j2 <= delay_bound (job_task j2)DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2
t1 <= job_arrival j2 < t2
apply : job_arrival_between; last exact : ARR2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 BOUND : forall j2 : Job2,
job_task j2 \in ts2 ->
arrives_in arr_seq1 (job1_of j2) ->
arrival_delay j2 <= delay_bound (job_task j2)DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2
consistent_arrival_times arr_seq2
exact : consistent_propagated_arrival_sequence. } Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 BOUND : forall j2 : Job2,
job_task j2 \in ts2 ->
arrives_in arr_seq1 (job1_of j2) ->
arrival_delay j2 <= delay_bound (job_task j2)DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2 j2t1 : t1 <= job_arrival j2 j2t2 : job_arrival j2 < t2
t1 - delay_bound tsk2 <= job_arrival j1 < t2
have BARR2: job_arrival j2 = job_arrival j1 + arrival_delay j2
by rewrite EQ; apply : DEF.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 BOUND : forall j2 : Job2,
job_task j2 \in ts2 ->
arrives_in arr_seq1 (job1_of j2) ->
arrival_delay j2 <= delay_bound (job_task j2)DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2 j2t1 : t1 <= job_arrival j2 j2t2 : job_arrival j2 < t2 BARR2 : job_arrival j2 =
job_arrival j1 + arrival_delay j2
t1 - delay_bound tsk2 <= job_arrival j1 < t2
suff : arrival_delay j2 <= delay_bound tsk2; first by lia .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 BOUND : forall j2 : Job2,
job_task j2 \in ts2 ->
arrives_in arr_seq1 (job1_of j2) ->
arrival_delay j2 <= delay_bound (job_task j2)DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2 j2t1 : t1 <= job_arrival j2 j2t2 : job_arrival j2 < t2 BARR2 : job_arrival j2 =
job_arrival j1 + arrival_delay j2
arrival_delay j2 <= delay_bound tsk2
rewrite -SRC2; apply : BOUND.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2 j2t1 : t1 <= job_arrival j2 j2t2 : job_arrival j2 < t2 BARR2 : job_arrival j2 =
job_arrival j1 + arrival_delay j2
job_task j2 \in ts2
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2 j2t1 : t1 <= job_arrival j2 j2t2 : job_arrival j2 < t2 BARR2 : job_arrival j2 =
job_arrival j1 + arrival_delay j2
job_task j2 \in ts2
by rewrite SRC2.
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 DEF : forall j2 : Job2,
job_arrival j2 =
job_arrival (job1_of j2) + arrival_delay j2j1 : Job1 j2 : Job2 ARR2 : j2 \in arrivals_between arr_seq2 t1 t2 EQ : j1 = job1_of j2 SRC2 : job_task j2 = tsk2 j2t1 : t1 <= job_arrival j2 j2t2 : job_arrival j2 < t2 BARR2 : job_arrival j2 =
job_arrival j1 + arrival_delay j2
arrives_in arr_seq1 (job1_of j2)
exact /arrives_in_propagated_only_if/in_arrivals_implies_arrived.
Qed .
(** Let [tsk1] denote the associated type-one task of [tsk1]... *)
Let tsk1 := task1_of tsk2.
(** ... and let [tsk1_arrivals] denote its jobs in the window during which
triggering jobs may arrive. *)
Let tsk1_arrivals := task_arrivals_between arr_seq1 tsk1 (t1 - delay_bound tsk2) t2.
(** The triggering jobs are hence a subset of all of [tsk1]'s arrivals. *)
Lemma subset_trigger_jobs :
{subset trigger_jobs <= tsk1_arrivals}.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
{subset trigger_jobs <= tsk1_arrivals}
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
{subset trigger_jobs <= tsk1_arrivals}
move => j1 IN.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs
j1 \in tsk1_arrivals
move : (IN) => /mapP [j2 /[!mem_filter]/andP[] TSK2 SRC2 MAP].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs j2 : Job2 TSK2 : job_of_task tsk2 j2 SRC2 : j2 \in arrivals_between arr_seq2 t1 t2 MAP : j1 = job1_of j2
job_of_task tsk1 j1 &&
(j1
\in arrivals_between arr_seq1
(t1 - delay_bound tsk2) t2)
apply /andP; split .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs j2 : Job2 TSK2 : job_of_task tsk2 j2 SRC2 : j2 \in arrivals_between arr_seq2 t1 t2 MAP : j1 = job1_of j2
job_of_task tsk1 j1
{ Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs j2 : Job2 TSK2 : job_of_task tsk2 j2 SRC2 : j2 \in arrivals_between arr_seq2 t1 t2 MAP : j1 = job1_of j2
job_of_task tsk1 j1
move : H_valid_mapping => [CONS _].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs j2 : Job2 TSK2 : job_of_task tsk2 j2 SRC2 : j2 \in arrivals_between arr_seq2 t1 t2 MAP : j1 = job1_of j2 CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)
job_of_task tsk1 j1
move : TSK2; rewrite /tsk1 /job_of_task MAP => /eqP <-.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs j2 : Job2 SRC2 : j2 \in arrivals_between arr_seq2 t1 t2 MAP : j1 = job1_of j2 CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)
job_task (job1_of j2) == task1_of (job_task j2)
by apply /eqP/CONS. } Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs j2 : Job2 TSK2 : job_of_task tsk2 j2 SRC2 : j2 \in arrivals_between arr_seq2 t1 t2 MAP : j1 = job1_of j2
j1
\in arrivals_between arr_seq1
(t1 - delay_bound tsk2) t2
{ Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs j2 : Job2 TSK2 : job_of_task tsk2 j2 SRC2 : j2 \in arrivals_between arr_seq2 t1 t2 MAP : j1 = job1_of j2
j1
\in arrivals_between arr_seq1
(t1 - delay_bound tsk2) t2
have /andP[Hge Hlt] := trigger_job_arrival_bounded j1 IN.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs j2 : Job2 TSK2 : job_of_task tsk2 j2 SRC2 : j2 \in arrivals_between arr_seq2 t1 t2 MAP : j1 = job1_of j2 Hge : t1 - delay_bound tsk2 <= job_arrival j1 Hlt : job_arrival j1 < t2
j1
\in arrivals_between arr_seq1
(t1 - delay_bound tsk2) t2
apply : job_in_arrivals_between => // /[!MAP].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j1 : Job1 IN : j1 \in trigger_jobs j2 : Job2 TSK2 : job_of_task tsk2 j2 SRC2 : j2 \in arrivals_between arr_seq2 t1 t2 MAP : j1 = job1_of j2 Hge : t1 - delay_bound tsk2 <= job_arrival j1 Hlt : job_arrival j1 < t2
arrives_in arr_seq1 (job1_of j2)
exact /arrives_in_propagated_only_if/in_arrivals_implies_arrived. }
Qed .
(** Additionally, from the assumption that each type-one job has at most one
type-two successor ([H_job2_of_singleton]), we have that [job1_of] is
injective (for the jobs in the arrival sequence). *)
Lemma job1_of_inj : {in tsk2_arrivals &, injective [eta job1_of]}.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
{in tsk2_arrivals &, injective [eta job1_of]}
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
{in tsk2_arrivals &, injective [eta job1_of]}
move => j2 j2' IN2 IN2' EQ.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2'
j2 = j2'
move : H_valid_mapping => [CONS _].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)
j2 = j2'
move : H_arr_seq_mapping => [CONS' _ _ _].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1
j2 = j2'
have SIZE: size (job2_of (job1_of j2')) <= 1 .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1
size (job2_of (job1_of j2')) <= 1
{ Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1
size (job2_of (job1_of j2')) <= 1
apply : (H_job2_of_singleton (task1_of (job_task j2'))).Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1
task1_of (job_task j2') \in ts1
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1
task1_of (job_task j2') \in ts1
rewrite /ts1 map_f //.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1
job_task j2' \in ts2
by move : IN2'; rewrite mem_filter /job_of_task => /andP [/eqP-> _].
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1
job_task (job1_of j2') = task1_of (job_task j2')
exact : CONS. } Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1SIZE : size (job2_of (job1_of j2')) <= 1
j2 = j2'
have : j2' \in job2_of (job1_of j2') by rewrite CONS'.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1SIZE : size (job2_of (job1_of j2')) <= 1
j2' \in job2_of (job1_of j2') -> j2 = j2'
move : SIZE (EQ); rewrite -CONS'.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1
size (job2_of (job1_of j2')) <= 1 ->
j2 \in job2_of (job1_of j2') ->
j2' \in job2_of (job1_of j2') -> j2 = j2'
case : (job2_of _) => [//|j2'' tail].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1j2'' : Job2 tail : seq Job2
size (j2'' :: tail) <= 1 ->
j2 \in j2'' :: tail ->
j2' \in j2'' :: tail -> j2 = j2'
case : tail => // _.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1 j2, j2' : Job2 IN2 : j2 \in tsk2_arrivals IN2' : j2' \in tsk2_arrivals EQ : job1_of j2 = job1_of j2' CONS : forall j2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2)CONS' : forall (j1 : Job1) (j2 : Job2),
j2 \in job2_of j1 <-> job1_of j2 = j1j2'' : Job2
j2 \in [:: j2''] -> j2' \in [:: j2''] -> j2 = j2'
by rewrite !mem_seq1 => /eqP-> /eqP->.
Qed .
(** Finally, the sequence of triggering jobs contains no duplicates since it
is part of the valid arrival sequence [arr_seq1]. *)
Lemma uniq_trigger_jobs : uniq trigger_jobs.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
uniq trigger_jobs
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
uniq trigger_jobs
rewrite map_inj_in_uniq; last exact : job1_of_inj.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
uniq tsk2_arrivals
rewrite filter_uniq //.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
uniq (arrivals_between arr_seq2 t1 t2)
apply : arrivals_uniq.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
consistent_arrival_times arr_seq2
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
consistent_arrival_times arr_seq2
exact : consistent_propagated_arrival_sequence.
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
arrival_sequence_uniq arr_seq2
exact : propagated_arrival_sequence_uniq.
Qed .
(** Taken together, the above facts allow us to conclude that the magnitude
of [trigger_jobs] is upper-bounded by the total number of jobs released
by [tsk1] during <<[t1 - delay_bound tsk2, t2]>>, i.e., the count of
jobs in [tsk1_arrivals]. *)
Corollary trigger_job_size : size trigger_jobs <= size tsk1_arrivals.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
size trigger_jobs <= size tsk1_arrivals
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
size trigger_jobs <= size tsk1_arrivals
apply : uniq_leq_size.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
uniq trigger_jobs
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
uniq trigger_jobs
exact : uniq_trigger_jobs.
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 t1, t2 : instant H_ordered : t1 <= t2 tsk2 : Task2 H_in_ts : tsk2 \in ts2 tsk2_arrivals := task_arrivals_between arr_seq2 tsk2 t1
t2 : seq Job2 trigger_jobs := [seq job1_of j2 | j2 <- tsk2_arrivals] : seq Job1 tsk1 := task1_of tsk2 : Task1 tsk1_arrivals := task_arrivals_between arr_seq1 tsk1
(t1 - delay_bound tsk2) t2 : seq Job1
{subset trigger_jobs <= tsk1_arrivals}
exact : subset_trigger_jobs.
Qed .
End ArrivalCurveCorrectnessSteps .
(** Assuming that the given arrival sequence for type-one tasks correctly
bounds the arrivals of triggering jobs, [trigger_job_size] implies that
the derived arrival curve correctly bounds the arrivals of type-two job
since [size tsk1_arrivals] is then bounded by the given arrival curve
[max_arrivals1]. *)
Theorem propagated_arrival_curve_respected :
taskset_respects_max_arrivals arr_seq1 ts1 ->
taskset_respects_max_arrivals arr_seq2 ts2.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1
taskset_respects_max_arrivals arr_seq1 ts1 ->
taskset_respects_max_arrivals arr_seq2 ts2
Proof .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1
taskset_respects_max_arrivals arr_seq1 ts1 ->
taskset_respects_max_arrivals arr_seq2 ts2
move => RESP1 tsk2 IN2 t1 t2 LEQ.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2
number_of_task_arrivals arr_seq2 tsk2 t1 t2 <=
max_arrivals tsk2 (t2 - t1)
have IN1 : task1_of tsk2 \in ts1 by rewrite /ts1 map_f.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1
number_of_task_arrivals arr_seq2 tsk2 t1 t2 <=
max_arrivals tsk2 (t2 - t1)
rewrite /max_arrivals/max_arrivals2/propagated_arrival_curve
/number_of_task_arrivals/task_arrivals_between.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1
size
[seq j <- arrivals_between arr_seq2 t1 t2
| job_of_task tsk2 j] <=
match t2 - t1 with
| 0 => 0
| _.+1 =>
max_arrivals (task1_of tsk2)
(t2 - t1 + delay_bound tsk2)
end
case DELTA: (t2 - t1) => [|D];
first by rewrite arrivals_between_geq //=; lia .Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1 D : nat DELTA : t2 - t1 = D.+1
size
[seq j <- arrivals_between arr_seq2 t1 t2
| job_of_task tsk2 j] <=
max_arrivals (task1_of tsk2) (D.+1 + delay_bound tsk2)
rewrite -DELTA => {D} {DELTA}.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1
size
[seq j <- arrivals_between arr_seq2 t1 t2
| job_of_task tsk2 j] <=
max_arrivals (task1_of tsk2)
(t2 - t1 + delay_bound tsk2)
rewrite -(size_map job1_of) //.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1
size
[seq job1_of i
| i <- arrivals_between arr_seq2 t1 t2
& job_of_task tsk2 i] <=
max_arrivals (task1_of tsk2)
(t2 - t1 + delay_bound tsk2)
apply : leq_trans; first exact : trigger_job_size.Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1
size
(task_arrivals_between arr_seq1 (task1_of tsk2)
(t1 - delay_bound tsk2) t2) <=
max_arrivals (task1_of tsk2)
(t2 - t1 + delay_bound tsk2)
apply (@leq_trans (max_arrivals (task1_of tsk2)
(t2 - (t1 - delay_bound tsk2)))).Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1
size
(task_arrivals_between arr_seq1 (task1_of tsk2)
(t1 - delay_bound tsk2) t2) <=
max_arrivals (task1_of tsk2)
(t2 - (t1 - delay_bound tsk2))
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1
size
(task_arrivals_between arr_seq1 (task1_of tsk2)
(t1 - delay_bound tsk2) t2) <=
max_arrivals (task1_of tsk2)
(t2 - (t1 - delay_bound tsk2))
rewrite -/(number_of_task_arrivals _ _ (t1 - delay_bound tsk2) t2).Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1
number_of_task_arrivals arr_seq1 (task1_of tsk2)
(t1 - delay_bound tsk2) t2 <=
max_arrivals (task1_of tsk2)
(t2 - (t1 - delay_bound tsk2))
by apply : (RESP1 _ IN1); lia .
- Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1
max_arrivals (task1_of tsk2)
(t2 - (t1 - delay_bound tsk2)) <=
max_arrivals (task1_of tsk2)
(t2 - t1 + delay_bound tsk2)
move : (H_valid_ac _ IN1) => [_ MONO].Task1, Task2 : TaskType Job1, Job2 : JobType H : JobTask Job1 Task1 H0 : JobTask Job2 Task2 JA1 : JobArrival Job1 JA2 : JobArrival Job2 job1_of : Job2 -> Job1 task1_of : Task2 -> Task1 job2_of : Job1 -> seq Job2 arrival_delay : Job2 -> duration delay_bound : Task2 -> duration ts2 : seq Task2 H_valid_mapping : valid_delay_propagation_mapping JA1
JA2 job1_of task1_of delay_bound
ts2 max_arrivals1 : MaxArrivals Task1 arr_seq1 : arrival_sequence Job1 H_arr_seq_mapping : valid_arr_seq_propagation_mapping
JA1 JA2 job1_of delay_bound
arr_seq1 job2_of arrival_delay
ts2 arr_seq2 := propagated_arrival_sequence JA1 job1_of
arr_seq1 job2_of arrival_delay : instant -> seq Job2 ts1 := [seq task1_of tsk2 | tsk2 <- ts2] : seq Task1 H_job2_of_singleton : forall tsk1 : Task1,
tsk1 \in ts1 ->
forall j1 : Job1,
job_task j1 = tsk1 ->
size (job2_of j1) <= 1 H_valid_arr_seq : valid_arrival_sequence arr_seq1 H_valid_ac : valid_taskset_arrival_curve ts1
max_arrivals1 RESP1 : taskset_respects_max_arrivals arr_seq1 ts1 tsk2 : Task2 IN2 : tsk2 \in ts2 t1, t2 : instant LEQ : t1 <= t2 IN1 : task1_of tsk2 \in ts1 MONO : monotone leq (max_arrivals1 (task1_of tsk2))
max_arrivals (task1_of tsk2)
(t2 - (t1 - delay_bound tsk2)) <=
max_arrivals (task1_of tsk2)
(t2 - t1 + delay_bound tsk2)
by apply : MONO; lia .
Qed .
End ACPropFacts .