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.
[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]
(** * Job Arrival Sequence in the Sporadic Model *) (** In this file, we prove basic facts about a task's arrival sequence in the sporadic task model. *) Section SporadicArrivals. (** Consider sporadic tasks ... *) Context {Task : TaskType} `{SporadicModel Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}. (** Consider any unique arrival sequence with consistent arrivals, ... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq. (** ... and any sporadic task [tsk] to be analyzed. *) Variable tsk : Task. (** Assume all tasks have valid minimum inter-arrival times, valid offsets, and respect the sporadic task model. *) Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk. Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk. (** Consider any two jobs from the arrival sequence that stem from task [tsk]. *) Variable j1 j2 : Job. Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1. Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2. Hypothesis H_j1_task: job_task j1 = tsk. Hypothesis H_j2_task: job_task j2 = tsk. (** We show that a sporadic task with valid min inter-arrival time cannot have more than one job arriving at any time. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

(exists j : Job, 1 < size (task_arrivals_at_job_arrival arr_seq j) /\ respects_sporadic_task_model arr_seq (job_task j) /\ valid_task_min_inter_arrival_time (job_task j)) -> False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

(exists j : Job, 1 < size (task_arrivals_at_job_arrival arr_seq j) /\ respects_sporadic_task_model arr_seq (job_task j) /\ valid_task_min_inter_arrival_time (job_task j)) -> False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
EXISTS_TWO: 1 < size (task_arrivals_at_job_arrival arr_seq j) -> uniq (task_arrivals_at_job_arrival arr_seq j) -> exists a b : Job, a <> b /\ a \in task_arrivals_at_job_arrival arr_seq j /\ b \in task_arrivals_at_job_arrival arr_seq j

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
EXISTS_TWO: 1 < size (task_arrivals_at_job_arrival arr_seq j) -> uniq (task_arrivals_at_job_arrival arr_seq j) -> exists a b : Job, a <> b /\ a \in task_arrivals_at_job_arrival arr_seq j /\ b \in task_arrivals_at_job_arrival arr_seq j
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
A_IN: a \in task_arrivals_at_job_arrival arr_seq j
B_IN: b \in task_arrivals_at_job_arrival arr_seq j

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
A_IN: job_of_task (job_task j) a && (a \in arrivals_at arr_seq (job_arrival j))
B_IN: job_of_task (job_task j) b && (b \in arrivals_at arr_seq (job_arrival j))

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = job_task j
ARRA: a \in arrivals_at arr_seq (job_arrival j)
TSKB: job_task b = job_task j
ARRB: b \in arrivals_at arr_seq (job_arrival j)

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = job_task j
ARRA: a \in arrivals_at arr_seq (job_arrival j)
TSKB: job_task b = job_task j
ARRB: b \in arrivals_at arr_seq (job_arrival j)
A_IN: b \in arr_seq (job_arrival j)
B_IN: a \in arr_seq (job_arrival j)

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = job_task j
ARRA: a \in arrivals_at arr_seq (job_arrival j)
TSKB: job_task b = job_task j
ARRB: b \in arrivals_at arr_seq (job_arrival j)
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = job_task j
ARRA: a \in arrivals_at arr_seq (job_arrival j)
TSKB: job_task b = job_task j
ARRB: b \in arrivals_at arr_seq (job_arrival j)
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
EQ_ARR_A: job_arrival a = job_arrival j

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: a <> b
TSKA: job_task a = job_task j
ARRA: a \in arrivals_at arr_seq (job_arrival j)
TSKB: job_task b = job_task j
ARRB: b \in arrivals_at arr_seq (job_arrival j)
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
EQ_ARR_A: job_arrival a = job_arrival j
EQ_ARR_B: job_arrival b = job_arrival j

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
j: Job
SIZE_G: 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC: respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA: valid_task_min_inter_arrival_time (job_task j)
CONSISTENT: consistent_arrival_times arr_seq
UNIQ: arrival_sequence_uniq arr_seq
a, b: Job
NEQ: job_arrival a <> job_arrival b
TSKA: job_task a = job_task j
ARRA: a \in arrivals_at arr_seq (job_arrival j)
TSKB: job_task b = job_task j
ARRB: b \in arrivals_at arr_seq (job_arrival j)
A_IN: arrives_in arr_seq b
B_IN: arrives_in arr_seq a
EQ_ARR_A: job_arrival a = job_arrival j
EQ_ARR_B: job_arrival b = job_arrival j

False
by rewrite EQ_ARR_A EQ_ARR_B in NEQ. Qed. (** We show that no jobs of the task [tsk] other than [j1] arrive at the same time as [j1], and thus the task arrivals at [job arrival j1] consists only of job [j1]. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

task_arrivals_at_job_arrival arr_seq j1 = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

task_arrivals_at_job_arrival arr_seq j1 = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job

seq = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq

seq = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
SIZE_CASE: size seq = 0 \/ size seq = 1 \/ 1 < size seq

seq = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
Z: size seq = 0

seq = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
ONE: size seq = 1
seq = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
GTONE: 1 < size seq
seq = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
Z: size seq = 0

seq = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
Z: seq = [::]

seq = [:: j1]
by rewrite Z in J_IN_FILTER.
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
ONE: size seq = 1

seq = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
s: Job
J_ONE: size [:: s] = 1

j1 \in [:: s] -> [:: s] = [:: j1]
by rewrite mem_seq1 => /eqP ->.
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
GTONE: 1 < size seq

seq = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
GTONE: 1 < size seq

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
GTONE: 1 < size seq

exists j : Job, 1 < size (task_arrivals_at_job_arrival arr_seq j) /\ respects_sporadic_task_model arr_seq (job_task j) /\ valid_task_min_inter_arrival_time (job_task j)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
seq:= task_arrivals_at_job_arrival arr_seq j1: seq.seq Job
J_IN_FILTER: j1 \in seq
GTONE: 1 < size seq

1 < size (task_arrivals_at_job_arrival arr_seq j1) /\ respects_sporadic_task_model arr_seq (job_task j1) /\ valid_task_min_inter_arrival_time (job_task j1)
by repeat split => //; try rewrite H_j1_task. Qed. (** We show that no jobs of the task [tsk] other than [j1] arrive at the same time as [j1], and thus the task arrivals at [job arrival j1] consists only of job [j1]. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

forall t : instant, job_arrival j1 = t -> task_arrivals_at arr_seq tsk t = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

forall t : instant, job_arrival j1 = t -> task_arrivals_at arr_seq tsk t = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
t: instant
ARR: job_arrival j1 = t

task_arrivals_at arr_seq tsk t = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
t: instant
ARR: job_arrival j1 = t

task_arrivals_at arr_seq tsk (job_arrival j1) = [:: j1]
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
t: instant
ARR: job_arrival j1 = t
J_AT: task_arrivals_at_job_arrival arr_seq j1 = [:: j1]

task_arrivals_at arr_seq tsk (job_arrival j1) = [:: j1]
by rewrite /task_arrivals_at_job_arrival H_j1_task in J_AT. Qed. (** We show that a job [j1] is the first job that arrives in task arrivals at [job_arrival j1] by showing that the index of job [j1] in [task_arrivals_at_job_arrival arr_seq j1] is 0. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0
by rewrite only_j_in_task_arrivals_at_j //= eq_refl. Qed. (** We observe that for any job [j] the arrival time of [prev_job j] is strictly less than the arrival time of [j] in context of periodic tasks. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

0 < job_index arr_seq j1 -> job_arrival (prev_job arr_seq j1) < job_arrival j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

0 < job_index arr_seq j1 -> job_arrival (prev_job arr_seq j1) < job_arrival j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1

job_arrival (prev_job arr_seq j1) < job_arrival j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1

job_arrival (prev_job arr_seq j1) < job_arrival j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1

job_arrival (prev_job arr_seq j1) != job_arrival j1 /\ job_arrival (prev_job arr_seq j1) <= job_arrival j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1

job_arrival (prev_job arr_seq j1) <> job_arrival j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1

arrives_in arr_seq (prev_job arr_seq j1)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1
job_task (prev_job arr_seq j1) = job_task j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1
prev_job arr_seq j1 <> j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1

arrives_in arr_seq (prev_job arr_seq j1)
by apply prev_job_arr.
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1

job_task (prev_job arr_seq j1) = job_task j1
by apply prev_job_task.
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1

prev_job arr_seq j1 <> j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1
EQ: prev_job arr_seq j1 = j1

False
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
IND: 0 < job_index arr_seq j1
PREV_ARR_LTE: job_arrival (prev_job arr_seq j1) <= job_arrival j1
EQ: prev_job arr_seq j1 = j1
SM_IND: job_index arr_seq j1 - 1 = job_index arr_seq j1

False
by lia. Qed. (** We show that task arrivals at [job_arrival j1] is the same as task arrivals that arrive between [job_arrival j1] and [job_arrival j1 + 1]. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

[seq j <- arrivals_at arr_seq (job_arrival j1) | job_of_task (job_task j1) j] = [seq j <- \cat_(job_arrival j1<=t<(job_arrival j1).+1) arrivals_at arr_seq t | job_of_task tsk j]
by rewrite big_nat1 H_j1_task. Qed. (** We show that the task arrivals up to the previous job [j1] concatenated with the sequence [::j1] (the sequence containing only the job [j1]) is same as task arrivals up to [job_arrival j1]. *)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

0 < job_index arr_seq j1 -> task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [:: j1] = task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk

0 < job_index arr_seq j1 -> task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [:: j1] = task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
JIND: 0 < job_index arr_seq j1

task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [:: j1] = task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
JIND: 0 < job_index arr_seq j1

task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1 = task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
JIND: 0 < job_index arr_seq j1

task_arrivals_up_to arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)) ++ task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1 = task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
JIND: 0 < job_index arr_seq j1

task_arrivals_up_to arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)) ++ task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1 = task_arrivals_up_to arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)) ++ task_arrivals_between arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)).+1 (job_arrival j1).+1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
JIND: 0 < job_index arr_seq j1

task_arrivals_up_to arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)) ++ task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1 = task_arrivals_up_to arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)) ++ task_arrivals_between arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)).+1 (job_arrival j1) ++ task_arrivals_between arr_seq (job_task j1) (job_arrival j1) (job_arrival j1).+1
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_j1_task: job_task j1 = tsk
H_j2_task: job_task j2 = tsk
JIND: 0 < job_index arr_seq j1

task_arrivals_up_to arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)) ++ task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1 = task_arrivals_up_to arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)) ++ [::] ++ task_arrivals_between arr_seq (job_task j1) (job_arrival j1) (job_arrival j1).+1
by rewrite cat0s H_j1_task. Qed. End SporadicArrivals.