Library prosa.analysis.facts.sporadic


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)

Require Export prosa.model.task.arrival.periodic.
Require Export prosa.analysis.facts.job_index.

The Sporadic Model

In this section we prove a few basic properties involving job indices in context of the sporadic model.
Section SporadicModelIndexLemmas.

Consider sporadic tasks with an offset ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{TaskMaxInterArrival Task}.
  Context `{SporadicModel Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any unique arrival sequence with consistent arrivals, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.

... and any sporadic task [tsk] that is to be analyzed.
  Variable tsk : Task.
  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 : Job.
  Variable j2 : Job.
  Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
  Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
  Hypothesis H_j1_task: job_task j1 = tsk.
  Hypothesis H_j2_task: job_task j2 = tsk.

We first show that for any two jobs [j1] and [j2], [j2] arrives after [j1] provided [job_index] of [j2] strictly exceeds the [job_index] of [j1].
  Lemma lower_index_implies_earlier_arrival:
      job_index arr_seq j1 < job_index arr_seq j2 →
      job_arrival j1 < job_arrival j2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 366)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  ============================
  job_index arr_seq j1 < job_index arr_seq j2 ->
  job_arrival j1 < job_arrival j2

----------------------------------------------------------------------------- *)

  Proof.
    intro IND.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 367)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  IND : job_index arr_seq j1 < job_index arr_seq j2
  ============================
  job_arrival j1 < job_arrival j2

----------------------------------------------------------------------------- *)

    move: (H_sporadic_model j1 j2) ⇒ SPORADIC; feed_n 6 SPORADIC ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 370)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  IND : job_index arr_seq j1 < job_index arr_seq j2
  SPORADIC : j1 <> j2 ->
             arrives_in arr_seq j1 ->
             arrives_in arr_seq j2 ->
             job_task j1 = tsk ->
             job_task j2 = tsk ->
             job_arrival j1 <= job_arrival j2 ->
             job_arrival j1 + task_min_inter_arrival_time tsk <=
             job_arrival j2
  ============================
  j1 <> j2

subgoal 2 (ID 400) is:
 job_arrival j1 <= job_arrival j2
subgoal 3 (ID 405) is:
 job_arrival j1 < job_arrival j2

----------------------------------------------------------------------------- *)

    - rewrite → diff_jobs_iff_diff_indices ⇒ //; auto.

(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals (ID 491)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  IND : job_index arr_seq j1 < job_index arr_seq j2
  SPORADIC : j1 <> j2 ->
             arrives_in arr_seq j1 ->
             arrives_in arr_seq j2 ->
             job_task j1 = tsk ->
             job_task j2 = tsk ->
             job_arrival j1 <= job_arrival j2 ->
             job_arrival j1 + task_min_inter_arrival_time tsk <=
             job_arrival j2
  ============================
  job_index arr_seq j1 <> job_index arr_seq j2

subgoal 2 (ID 497) is:
 job_task j1 = job_task j2
subgoal 3 (ID 400) is:
 job_arrival j1 <= job_arrival j2
subgoal 4 (ID 405) is:
 job_arrival j1 < job_arrival j2

----------------------------------------------------------------------------- *)

       + now ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 497)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  IND : job_index arr_seq j1 < job_index arr_seq j2
  SPORADIC : j1 <> j2 ->
             arrives_in arr_seq j1 ->
             arrives_in arr_seq j2 ->
             job_task j1 = tsk ->
             job_task j2 = tsk ->
             job_arrival j1 <= job_arrival j2 ->
             job_arrival j1 + task_min_inter_arrival_time tsk <=
             job_arrival j2
  ============================
  job_task j1 = job_task j2

subgoal 2 (ID 400) is:
 job_arrival j1 <= job_arrival j2
subgoal 3 (ID 405) is:
 job_arrival j1 < job_arrival j2

----------------------------------------------------------------------------- *)

       + now rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 400)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  IND : job_index arr_seq j1 < job_index arr_seq j2
  SPORADIC : job_arrival j1 <= job_arrival j2 ->
             job_arrival j1 + task_min_inter_arrival_time tsk <=
             job_arrival j2
  ============================
  job_arrival j1 <= job_arrival j2

subgoal 2 (ID 405) is:
 job_arrival j1 < job_arrival j2

----------------------------------------------------------------------------- *)

    - apply (index_lte_implies_arrival_lte arr_seq); try auto.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1427)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  IND : job_index arr_seq j1 < job_index arr_seq j2
  SPORADIC : job_arrival j1 <= job_arrival j2 ->
             job_arrival j1 + task_min_inter_arrival_time tsk <=
             job_arrival j2
  ============================
  job_task j2 = job_task j1

subgoal 2 (ID 405) is:
 job_arrival j1 < job_arrival j2

----------------------------------------------------------------------------- *)

      now rewrite H_j1_task.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 405)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  IND : job_index arr_seq j1 < job_index arr_seq j2
  SPORADIC : job_arrival j1 + task_min_inter_arrival_time tsk <=
             job_arrival j2
  ============================
  job_arrival j1 < job_arrival j2

----------------------------------------------------------------------------- *)

    - have POS_IA : task_min_inter_arrival_time tsk > 0 by auto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1437)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  IND : job_index arr_seq j1 < job_index arr_seq j2
  SPORADIC : job_arrival j1 + task_min_inter_arrival_time tsk <=
             job_arrival j2
  POS_IA : 0 < task_min_inter_arrival_time tsk
  ============================
  job_arrival j1 < job_arrival j2

----------------------------------------------------------------------------- *)

      now ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End SporadicModelIndexLemmas.

Different jobs have different arrival times.

Section DifferentJobsImplyDifferentArrivalTimes.

Consider sporadic tasks with an offset ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{TaskMaxInterArrival Task}.
  Context `{SporadicModel Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any unique arrival sequence with consistent arrivals, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.

... and any sporadic task [tsk] that is to be analyzed.
  Variable tsk : Task.
  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 : Job.
  Variable j2 : Job.
  Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
  Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
  Hypothesis H_j1_task: job_task j1 = tsk.
  Hypothesis H_j2_task: job_task j2 = tsk.

We observe that distinct jobs cannot have equal arrival times.
  Lemma uneq_job_uneq_arr:
      j1 ≠ j2 →
      job_arrival j1 ≠ job_arrival j2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 362)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  ============================
  j1 <> j2 -> job_arrival j1 <> job_arrival j2

----------------------------------------------------------------------------- *)

  Proof.
    intros UNEQ EQ_ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 365)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  UNEQ : j1 <> j2
  EQ_ARR : job_arrival j1 = job_arrival j2
  ============================
  False

----------------------------------------------------------------------------- *)

    rewrite → diff_jobs_iff_diff_indices in UNEQ ⇒ //; auto; last by rewrite H_j1_task.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 382)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  EQ_ARR : job_arrival j1 = job_arrival j2
  UNEQ : job_index arr_seq j1 <> job_index arr_seq j2
  ============================
  False

----------------------------------------------------------------------------- *)

    move /neqP: UNEQ; rewrite neq_ltn ⇒ /orP [LT|LT].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 625)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  EQ_ARR : job_arrival j1 = job_arrival j2
  LT : job_index arr_seq j1 < job_index arr_seq j2
  ============================
  False

subgoal 2 (ID 626) is:
 False

----------------------------------------------------------------------------- *)

    all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT ⇒ //; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We prove a stronger version of the above lemma by showing that jobs [j1] and [j2] are equal if and only if they arrive at the same time.
  Lemma same_jobs_iff_same_arr:
    j1 = j2 ↔
    job_arrival j1 = job_arrival j2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 371)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  ============================
  j1 = j2 <-> job_arrival j1 = job_arrival j2

----------------------------------------------------------------------------- *)

  Proof.
    split; first by apply congr1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 374)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  ============================
  job_arrival j1 = job_arrival j2 -> j1 = j2

----------------------------------------------------------------------------- *)

    intro EQ_ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 375)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  EQ_ARR : job_arrival j1 = job_arrival j2
  ============================
  j1 = j2

----------------------------------------------------------------------------- *)

    case: (boolP (j1 == j2)) ⇒ [/eqP EQ | /eqP NEQ]; first by auto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 463)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  EQ_ARR : job_arrival j1 = job_arrival j2
  NEQ : j1 <> j2
  ============================
  j1 = j2

----------------------------------------------------------------------------- *)

    rewrite → diff_jobs_iff_diff_indices in NEQ ⇒ //; auto; last by rewrite H_j1_task.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 480)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  EQ_ARR : job_arrival j1 = job_arrival j2
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  ============================
  j1 = j2

----------------------------------------------------------------------------- *)

    move /neqP: NEQ; rewrite neq_ltn ⇒ /orP [LT|LT].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 706)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : TaskMaxInterArrival Task
  H1 : SporadicModel Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arrseq : arrival_sequence_uniq 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_arrseq : arrives_in arr_seq j1
  H_j2_from_arrseq : arrives_in arr_seq j2
  H_j1_task : job_task j1 = tsk
  H_j2_task : job_task j2 = tsk
  EQ_ARR : job_arrival j1 = job_arrival j2
  LT : job_index arr_seq j1 < job_index arr_seq j2
  ============================
  j1 = j2

subgoal 2 (ID 707) is:
 j1 = j2

----------------------------------------------------------------------------- *)

    all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT ⇒ //; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End DifferentJobsImplyDifferentArrivalTimes.

In this section we prove a few properties regarding task arrivals in context of the sporadic task model.
Section SporadicArrivals.

Consider sporadic tasks with an offset ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{SporadicModel Task}.
  Context `{TaskMaxInterArrival Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any unique arrival sequence with consistent arrivals, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq 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.
  Hypothesis H_valid_offset: valid_offset arr_seq 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.
  Lemma size_task_arrivals_at_leq_one:
    (∃ j,
        size (task_arrivals_at_job_arrival arr_seq j) > 1 ∧
        respects_sporadic_task_model arr_seq (job_task j) ∧
        valid_task_min_inter_arrival_time (job_task j)) →
      False.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 379)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

  Proof.
    move ⇒ [j [SIZE_G [PERIODIC VALID_TMIA]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 410)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

    specialize (exists_two Job (task_arrivals_at_job_arrival arr_seq j)) ⇒ EXISTS_TWO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 417)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

    destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 442)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)
  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

----------------------------------------------------------------------------- *)

    rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 527)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)
  a, b : Job
  NEQ : a <> b
  A_IN : (job_task a == job_task j) &&
         (a \in arrivals_at arr_seq (job_arrival j))
  B_IN : (job_task b == job_task j) &&
         (b \in arrivals_at arr_seq (job_arrival j))
  ============================
  False

----------------------------------------------------------------------------- *)

    move: A_IN B_IN ⇒ /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 674)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)
  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

----------------------------------------------------------------------------- *)

    move: (ARRA); move: (ARRB); rewrite /arrivals_at ⇒ A_IN B_IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 681)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)
  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

----------------------------------------------------------------------------- *)

    apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 686)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)
  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

----------------------------------------------------------------------------- *)

    have EQ_ARR_A : (job_arrival a = job_arrival j) by apply H_consistent_arrivals.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 697)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)
  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

----------------------------------------------------------------------------- *)

    have EQ_ARR_B : (job_arrival b = job_arrival j) by apply H_consistent_arrivals.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 707)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)
  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

----------------------------------------------------------------------------- *)

    apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j) in NEQ ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 716)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)
  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

----------------------------------------------------------------------------- *)

    now rewrite EQ_ARR_A EQ_ARR_B in NEQ.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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].
  Lemma only_j_in_task_arrivals_at_j:
    task_arrivals_at_job_arrival arr_seq j1 = [::j1].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 388)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

----------------------------------------------------------------------------- *)

  Proof.
    set (task_arrivals_at_job_arrival arr_seq j1) as seq in ×.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 394)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

----------------------------------------------------------------------------- *)

    have J_IN_FILTER : (j1 \in seq) by apply arrives_in_task_arrivals_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 407)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

----------------------------------------------------------------------------- *)

    have SIZE_CASE : size seq = 0 ∨ size seq = 1 ∨ size seq > 1
      by intros; now destruct (size seq) as [ | [ | ]]; try auto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 471)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

----------------------------------------------------------------------------- *)

    move: SIZE_CASE ⇒ [Z|[ONE|GTONE]].

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 486)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

subgoal 2 (ID 499) is:
 seq = [:: j1]
subgoal 3 (ID 500) is:
 seq = [:: j1]

----------------------------------------------------------------------------- *)

    - apply size0nil in Z.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 501)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

subgoal 2 (ID 499) is:
 seq = [:: j1]
subgoal 3 (ID 500) is:
 seq = [:: j1]

----------------------------------------------------------------------------- *)

      now rewrite Z in J_IN_FILTER.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 499)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

subgoal 2 (ID 500) is:
 seq = [:: j1]

----------------------------------------------------------------------------- *)

    - repeat (destruct seq; try by done).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 620)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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_IN_FILTER : j1 \in [:: s]
  ONE : size [:: s] = 1
  ============================
  [:: s] = [:: j1]

subgoal 2 (ID 500) is:
 seq = [:: j1]

----------------------------------------------------------------------------- *)

      rewrite mem_seq1 in J_IN_FILTER; move : J_IN_FILTER ⇒ /eqP J1_S.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 743)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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
  ONE : size [:: s] = 1
  J1_S : j1 = s
  ============================
  [:: s] = [:: j1]

subgoal 2 (ID 500) is:
 seq = [:: j1]

----------------------------------------------------------------------------- *)

      now rewrite J1_S.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 500)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

----------------------------------------------------------------------------- *)

    - exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 746)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

      apply size_task_arrivals_at_leq_one.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 747)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)

----------------------------------------------------------------------------- *)

      ∃ j1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 749)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)

----------------------------------------------------------------------------- *)

      now repeat split ⇒ //; try rewrite H_j1_task.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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].
  Lemma only_j_at_job_arrival_j:
    ∀ t,
      job_arrival j1 = t →
      task_arrivals_at arr_seq tsk t = [::j1].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 401)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

----------------------------------------------------------------------------- *)

  Proof.
    intros t ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 403)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

----------------------------------------------------------------------------- *)

    rewrite -ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 405)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

----------------------------------------------------------------------------- *)

    specialize (only_j_in_task_arrivals_at_j) ⇒ J_AT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 408)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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]

----------------------------------------------------------------------------- *)

    now rewrite /task_arrivals_at_job_arrival H_j1_task in J_AT.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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.
  Lemma index_j_in_task_arrivals_at:
    index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 409)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

  Proof.
    now rewrite only_j_in_task_arrivals_at_j //= eq_refl.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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.
  Lemma prev_job_arr_lt:
    job_index arr_seq j1 > 0 →
    job_arrival (prev_job arr_seq j1) < job_arrival j1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 422)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

  Proof.
    intros IND.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 423)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

    have PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) ≤ job_arrival j1 by apply prev_job_arr_lte ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 441)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

    rewrite ltn_neqAle; apply /andP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 469)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

    split ⇒ //; apply /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 532)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

    apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j1) ⇒ //; try by rewrite H_j1_task.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 545)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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)

subgoal 2 (ID 547) is:
 job_task (prev_job arr_seq j1) = job_task j1
subgoal 3 (ID 549) is:
 prev_job arr_seq j1 <> j1

----------------------------------------------------------------------------- *)

    - now apply prev_job_arr.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 547)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

subgoal 2 (ID 549) is:
 prev_job arr_seq j1 <> j1

----------------------------------------------------------------------------- *)

    - now apply prev_job_task.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 549)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

    - intro EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 720)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

      have SM_IND: job_index arr_seq j1 - 1 = job_index arr_seq j1 by rewrite -prev_job_index // EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 775)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

      now ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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].
  Lemma task_arrivals_at_as_task_arrivals_between:
    task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 436)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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) (succn (job_arrival j1))

----------------------------------------------------------------------------- *)

  Proof.
    rewrite /task_arrivals_at_job_arrival /task_arrivals_at /task_arrivals_between /arrivals_between.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 462)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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_task j == job_task j1] =
  [seq j <- \cat_(job_arrival j1<=t<succn (job_arrival j1)|true)
             arrivals_at arr_seq t
     | job_task j == tsk]

----------------------------------------------------------------------------- *)

    now rewrite big_nat1 H_j1_task.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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].
  Lemma prev_job_cat:
    job_index arr_seq j1 > 0 →
    task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [::j1] = task_arrivals_up_to_job_arrival arr_seq j1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 458)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

  Proof.
    intros JIND.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 459)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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

----------------------------------------------------------------------------- *)

    rewrite -only_j_in_task_arrivals_at_j task_arrivals_at_as_task_arrivals_between.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 463)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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) (succn (job_arrival j1)) =
  task_arrivals_up_to_job_arrival arr_seq j1

----------------------------------------------------------------------------- *)

    rewrite /task_arrivals_up_to_job_arrival prev_job_task ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 487)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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) (succn (job_arrival j1)) =
  task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)

----------------------------------------------------------------------------- *)

    rewrite [in X in _ = X] (task_arrivals_cat _ _ (job_arrival (prev_job arr_seq j1))); last by
        apply ltnW; apply prev_job_arr_lt.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 550)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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) (succn (job_arrival j1)) =
  task_arrivals_up_to arr_seq (job_task j1)
    (job_arrival (prev_job arr_seq j1)) ++
  task_arrivals_between arr_seq (job_task j1)
    (succn (job_arrival (prev_job arr_seq j1))) (succn (job_arrival j1))

----------------------------------------------------------------------------- *)

    rewrite [in X in _ = _ ++ X] (task_arrivals_between_cat _ _ _ (job_arrival j1) _) ⇒ //; last by apply prev_job_arr_lt.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 597)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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) (succn (job_arrival j1)) =
  task_arrivals_up_to arr_seq (job_task j1)
    (job_arrival (prev_job arr_seq j1)) ++
  task_arrivals_between arr_seq (job_task j1)
    (succn (job_arrival (prev_job arr_seq j1))) (job_arrival j1) ++
  task_arrivals_between arr_seq (job_task j1) (job_arrival j1)
    (succn (job_arrival j1))

----------------------------------------------------------------------------- *)

    rewrite no_jobs_between_consecutive_jobs ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 660)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : SporadicModel Task
  H1 : TaskMaxInterArrival Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq 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
  H_valid_offset : valid_offset arr_seq 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) (succn (job_arrival j1)) =
  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)
    (succn (job_arrival j1))

----------------------------------------------------------------------------- *)

    now rewrite cat0s H_j1_task.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End SporadicArrivals.