Library prosa.analysis.facts.periodic.arrival_separation


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

Welcome to Coq 8.11.2 (June 2020)

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

Require Export prosa.analysis.facts.periodic.sporadic.
Require Export prosa.analysis.facts.sporadic.

In this section we show that the separation between job arrivals of a periodic task is some multiple of their corresponding task's period.
Section JobArrivalSeparation.

Consider periodic tasks with an offset ...
  Context {Task : TaskType}.
  Context `{PeriodicModel Task}.

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

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

... and any task [tsk] that is to be analyzed.
  Variable tsk : Task.

Assume all tasks have a valid period and respect the periodic task model.
  Hypothesis H_periodic_model: respects_periodic_task_model arr_seq tsk.
  Hypothesis H_valid_period: valid_period tsk.

In this section we show that two consecutive jobs of a periodic task have their arrival times separated by their task's period.
  Section ConsecutiveJobSeparation.

Consider any two _consecutive_ jobs [j1] and [j2] of task [tsk].
    Variable j1 : Job.
    Variable j2 : Job.
    Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
    Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
    Hypothesis H_j1_of_task: job_task j1 = tsk.
    Hypothesis H_j2_of_task: job_task j2 = tsk.
    Hypothesis H_consecutive_jobs: job_index arr_seq j2 = job_index arr_seq j1 + 1.

We show that if job [j1] and [j2] are consecutive jobs with [j2] arriving after [j1], then their arrival times are separated by their task's period.
    Lemma consecutive_job_separation:
      job_arrival j2 = job_arrival j1 + task_period tsk.

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

1 subgoal (ID 372)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
  ============================
  job_arrival j2 = job_arrival j1 + task_period tsk

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

    Proof.
      move : (H_periodic_model j2) ⇒ PERIODIC.

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

1 subgoal (ID 374)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
  PERIODIC : arrives_in arr_seq j2 ->
             0 < job_index arr_seq j2 ->
             job_task j2 = tsk ->
             exists j' : Job,
               arrives_in arr_seq j' /\
               job_index arr_seq j' = job_index arr_seq j2 - 1 /\
               job_task j' = tsk /\
               job_arrival j2 = job_arrival j' + task_period tsk
  ============================
  job_arrival j2 = job_arrival j1 + task_period tsk

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

      feed_n 3 PERIODIC ⇒ //; first by rewrite H_consecutive_jobs; ssrlia.

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

1 subgoal (ID 392)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
  PERIODIC : exists j' : Job,
               arrives_in arr_seq j' /\
               job_index arr_seq j' = job_index arr_seq j2 - 1 /\
               job_task j' = tsk /\
               job_arrival j2 = job_arrival j' + task_period tsk
  ============================
  job_arrival j2 = job_arrival j1 + task_period tsk

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

      move : PERIODIC ⇒ [pj' [ARR_IN_PJ' [INDPJ'J' [TSKPJ' ARRPJ']]]].

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

1 subgoal (ID 1060)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
  pj' : Job
  ARR_IN_PJ' : arrives_in arr_seq pj'
  INDPJ'J' : job_index arr_seq pj' = job_index arr_seq j2 - 1
  TSKPJ' : job_task pj' = tsk
  ARRPJ' : job_arrival j2 = job_arrival pj' + task_period tsk
  ============================
  job_arrival j2 = job_arrival j1 + task_period tsk

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

      rewrite H_consecutive_jobs addnK in INDPJ'J'.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1099)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
  pj' : Job
  ARR_IN_PJ' : arrives_in arr_seq pj'
  TSKPJ' : job_task pj' = tsk
  ARRPJ' : job_arrival j2 = job_arrival pj' + task_period tsk
  INDPJ'J' : job_index arr_seq pj' = job_index arr_seq j1
  ============================
  job_arrival j2 = job_arrival j1 + task_period tsk

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

      apply equal_index_implies_equal_jobs in INDPJ'J' ⇒ //; last by rewrite TSKPJ'.

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

1 subgoal (ID 1104)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
  pj' : Job
  ARR_IN_PJ' : arrives_in arr_seq pj'
  TSKPJ' : job_task pj' = tsk
  ARRPJ' : job_arrival j2 = job_arrival pj' + task_period tsk
  INDPJ'J' : pj' = j1
  ============================
  job_arrival j2 = job_arrival j1 + task_period tsk

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

      now rewrite INDPJ'J' in ARRPJ'; ssrlia.

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

No more subgoals.

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

    Qed.

  End ConsecutiveJobSeparation.

In this section we show that for two unequal jobs of a task, there exists a non-zero multiple of their task's period which separates their arrival times.
  Section ArrivalSeparationWithGivenIndexDifference.

Consider any two _consecutive_ jobs [j1] and [j2] of task [tsk] that stem from the arrival sequence.
    Variable j1 j2 : Job.
    Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
    Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
    Hypothesis H_j1_of_task: job_task j1 = tsk.
    Hypothesis H_j2_of_task: job_task j2 = tsk.

We'll assume that job [j1] arrives before [j2] and that their indices differ by an integer [k].
    Variable k : nat.
    Hypothesis H_index_difference_k: job_index arr_seq j1 + k = job_index arr_seq j2 .
    Hypothesis H_job_arrival_lt: job_arrival j1 < job_arrival j2.

We prove that arrival of unequal jobs of a task [tsk] are separated by a non-zero multiple of [task_period tsk] provided their index differs by a number [k].
    Lemma job_arrival_separation_when_index_diff_is_k:
      ∃ n,
        n > 0 ∧
        job_arrival j2 = job_arrival j1 + n × task_period tsk.

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

1 subgoal (ID 378)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  k : nat
  H_index_difference_k : job_index arr_seq j1 + k = job_index arr_seq j2
  H_job_arrival_lt : job_arrival j1 < job_arrival j2
  ============================
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

    Proof.
      move: j1 j2 H_j1_of_task H_j2_of_task H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq;
        clear H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq H_j1_of_task H_j2_of_task j1 j2.

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

1 subgoal (ID 387)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k : nat
  ============================
  forall j1 j2 : Job,
  job_task j1 = tsk ->
  job_task j2 = tsk ->
  job_index arr_seq j1 + k = job_index arr_seq j2 ->
  job_arrival j1 < job_arrival j2 ->
  arrives_in arr_seq j2 ->
  arrives_in arr_seq j1 ->
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

      move: k ⇒ s.

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

1 subgoal (ID 389)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  ============================
  forall j1 j2 : Job,
  job_task j1 = tsk ->
  job_task j2 = tsk ->
  job_index arr_seq j1 + s = job_index arr_seq j2 ->
  job_arrival j1 < job_arrival j2 ->
  arrives_in arr_seq j2 ->
  arrives_in arr_seq j1 ->
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

      induction s.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 393)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k : nat
  ============================
  forall j1 j2 : Job,
  job_task j1 = tsk ->
  job_task j2 = tsk ->
  job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
  job_arrival j1 < job_arrival j2 ->
  arrives_in arr_seq j2 ->
  arrives_in arr_seq j1 ->
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

subgoal 2 (ID 396) is:
 forall j1 j2 : Job,
 job_task j1 = tsk ->
 job_task j2 = tsk ->
 job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
 job_arrival j1 < job_arrival j2 ->
 arrives_in arr_seq j2 ->
 arrives_in arr_seq j1 ->
 exists n : nat,
   0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

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

1 subgoal (ID 393)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k : nat
  ============================
  forall j1 j2 : Job,
  job_task j1 = tsk ->
  job_task j2 = tsk ->
  job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
  job_arrival j1 < job_arrival j2 ->
  arrives_in arr_seq j2 ->
  arrives_in arr_seq j1 ->
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

intros j1 j2 TSKj1 TSKj2 STEP LT ARRj1 ARRj2; exfalso.

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

1 subgoal (ID 405)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k : nat
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj1 : arrives_in arr_seq j2
  ARRj2 : arrives_in arr_seq j1
  ============================
  False

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

        specialize (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals j1 j2) ⇒ LT_IND.

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

1 subgoal (ID 412)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k : nat
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj1 : arrives_in arr_seq j2
  ARRj2 : arrives_in arr_seq j1
  LT_IND : arrives_in arr_seq j1 ->
           arrives_in arr_seq j2 ->
           job_task j1 = job_task j2 ->
           job_arrival j1 < job_arrival j2 ->
           job_index arr_seq j1 < job_index arr_seq j2
  ============================
  False

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

        feed_n 4 LT_IND ⇒ //; first by rewrite TSKj2.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 436)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k : nat
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj1 : arrives_in arr_seq j2
  ARRj2 : arrives_in arr_seq j1
  LT_IND : job_index arr_seq j1 < job_index arr_seq j2
  ============================
  False

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


        now ssrlia.

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

1 subgoal (ID 396)

subgoal 1 (ID 396) is:
 forall j1 j2 : Job,
 job_task j1 = tsk ->
 job_task j2 = tsk ->
 job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
 job_arrival j1 < job_arrival j2 ->
 arrives_in arr_seq j2 ->
 arrives_in arr_seq j1 ->
 exists n : nat,
   0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

      }

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

1 subgoal (ID 396)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  IHs : forall j1 j2 : Job,
        job_task j1 = tsk ->
        job_task j2 = tsk ->
        job_index arr_seq j1 + s = job_index arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq j1 ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
  ============================
  forall j1 j2 : Job,
  job_task j1 = tsk ->
  job_task j2 = tsk ->
  job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
  job_arrival j1 < job_arrival j2 ->
  arrives_in arr_seq j2 ->
  arrives_in arr_seq j1 ->
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

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

1 subgoal (ID 396)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  IHs : forall j1 j2 : Job,
        job_task j1 = tsk ->
        job_task j2 = tsk ->
        job_index arr_seq j1 + s = job_index arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq j1 ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
  ============================
  forall j1 j2 : Job,
  job_task j1 = tsk ->
  job_task j2 = tsk ->
  job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
  job_arrival j1 < job_arrival j2 ->
  arrives_in arr_seq j2 ->
  arrives_in arr_seq j1 ->
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

intros j1 j2 TSKj1 TSKj2 STEP LT ARRj2 ARRj1.

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

1 subgoal (ID 679)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  IHs : forall j1 j2 : Job,
        job_task j1 = tsk ->
        job_task j2 = tsk ->
        job_index arr_seq j1 + s = job_index arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq j1 ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn s = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  ============================
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

        specialize (exists_jobs_before_j
                      arr_seq H_consistent_arrivals H_uniq_arrseq j2 ARRj2 (job_index arr_seq j2 - s)) ⇒ BEFORE.

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

1 subgoal (ID 690)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  IHs : forall j1 j2 : Job,
        job_task j1 = tsk ->
        job_task j2 = tsk ->
        job_index arr_seq j1 + s = job_index arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq j1 ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn s = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  BEFORE : job_index arr_seq j2 - s < job_index arr_seq j2 ->
           exists j' : Job,
             j2 <> j' /\
             job_task j' = job_task j2 /\
             arrives_in arr_seq j' /\
             job_index arr_seq j' = job_index arr_seq j2 - s
  ============================
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

        destruct s.

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

2 subgoals (ID 707)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k : nat
  IHs : forall j1 j2 : Job,
        job_task j1 = tsk ->
        job_task j2 = tsk ->
        job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq j1 ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + 1 = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  BEFORE : job_index arr_seq j2 - 0 < job_index arr_seq j2 ->
           exists j' : Job,
             j2 <> j' /\
             job_task j' = job_task j2 /\
             arrives_in arr_seq j' /\
             job_index arr_seq j' = job_index arr_seq j2 - 0
  ============================
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

subgoal 2 (ID 714) is:
 exists n : nat,
   0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

        - ∃ 1; repeat split.

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

2 subgoals (ID 719)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k : nat
  IHs : forall j1 j2 : Job,
        job_task j1 = tsk ->
        job_task j2 = tsk ->
        job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq j1 ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + 1 = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  BEFORE : job_index arr_seq j2 - 0 < job_index arr_seq j2 ->
           exists j' : Job,
             j2 <> j' /\
             job_task j' = job_task j2 /\
             arrives_in arr_seq j' /\
             job_index arr_seq j' = job_index arr_seq j2 - 0
  ============================
  job_arrival j2 = job_arrival j1 + 1 * task_period tsk

subgoal 2 (ID 714) is:
 exists n : nat,
   0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

          now rewrite (consecutive_job_separation j1) //; ssrlia.

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

1 subgoal (ID 714)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  IHs : forall j1 j2 : Job,
        job_task j1 = tsk ->
        job_task j2 = tsk ->
        job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq j1 ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  BEFORE : job_index arr_seq j2 - succn s < job_index arr_seq j2 ->
           exists j' : Job,
             j2 <> j' /\
             job_task j' = job_task j2 /\
             arrives_in arr_seq j' /\
             job_index arr_seq j' = job_index arr_seq j2 - succn s
  ============================
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

        - feed BEFORE; first by ssrlia.

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

1 subgoal (ID 1751)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  IHs : forall j1 j2 : Job,
        job_task j1 = tsk ->
        job_task j2 = tsk ->
        job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq j1 ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  BEFORE : exists j' : Job,
             j2 <> j' /\
             job_task j' = job_task j2 /\
             arrives_in arr_seq j' /\
             job_index arr_seq j' = job_index arr_seq j2 - succn s
  ============================
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

          move : BEFORE ⇒ [nj [NEQNJ [TSKNJ [ARRNJ INDNJ]]]]; rewrite TSKj2 in TSKNJ.

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

1 subgoal (ID 2838)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  IHs : forall j1 j2 : Job,
        job_task j1 = tsk ->
        job_task j2 = tsk ->
        job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq j1 ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
  j1, j2 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  nj : Job
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  ============================
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

          specialize (IHs nj j2); feed_n 6 IHs ⇒ //; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 2859)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj : Job
  IHs : job_arrival nj < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq nj ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival nj + n * task_period tsk
  j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  ============================
  job_arrival nj < job_arrival j2

subgoal 2 (ID 2876) is:
 exists n : nat,
   0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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


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

1 subgoal (ID 2859)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj : Job
  IHs : job_arrival nj < job_arrival j2 ->
        arrives_in arr_seq j2 ->
        arrives_in arr_seq nj ->
        exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival nj + n * task_period tsk
  j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  ============================
  job_arrival nj < job_arrival j2

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

now apply (lower_index_implies_earlier_arrival _ H_consistent_arrivals H_uniq_arrseq tsk);
              auto with basic_facts; ssrlia.

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

1 subgoal (ID 2876)

subgoal 1 (ID 2876) is:
 exists n : nat,
   0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

          }

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

1 subgoal (ID 2876)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj : Job
  IHs : exists n : nat,
          0 < n /\ job_arrival j2 = job_arrival nj + n * task_period tsk
  j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  ============================
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

          move : IHs ⇒ [n [NZN ARRJ'NJ]].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 5209)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj, j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  n : nat
  NZN : 0 < n
  ARRJ'NJ : job_arrival j2 = job_arrival nj + n * task_period tsk
  ============================
  exists n0 : nat,
    0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk

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


          move: (H_periodic_model nj) ⇒ PERIODIC; feed_n 3 PERIODIC ⇒ //; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 5229)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj, j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  n : nat
  NZN : 0 < n
  ARRJ'NJ : job_arrival j2 = job_arrival nj + n * task_period tsk
  PERIODIC : exists j' : Job,
               arrives_in arr_seq j' /\
               job_index arr_seq j' = job_index arr_seq nj - 1 /\
               job_task j' = tsk /\
               job_arrival nj = job_arrival j' + task_period tsk
  ============================
  exists n0 : nat,
    0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk

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

          move : PERIODIC ⇒ [sj [ARR_IN_SJ [INDSJ [TSKSJ ARRSJ]]]]; rewrite ARRSJ in ARRJ'NJ.

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

1 subgoal (ID 7339)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj, j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  n : nat
  NZN : 0 < n
  sj : Job
  ARR_IN_SJ : arrives_in arr_seq sj
  INDSJ : job_index arr_seq sj = job_index arr_seq nj - 1
  TSKSJ : job_task sj = tsk
  ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
  ARRJ'NJ : job_arrival j2 =
            job_arrival sj + task_period tsk + n * task_period tsk
  ============================
  exists n0 : nat,
    0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk

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

          have INDJ : (job_index arr_seq j1 = job_index arr_seq j2 - s.+2) by ssrlia.

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

1 subgoal (ID 7888)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj, j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  n : nat
  NZN : 0 < n
  sj : Job
  ARR_IN_SJ : arrives_in arr_seq sj
  INDSJ : job_index arr_seq sj = job_index arr_seq nj - 1
  TSKSJ : job_task sj = tsk
  ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
  ARRJ'NJ : job_arrival j2 =
            job_arrival sj + task_period tsk + n * task_period tsk
  INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
  ============================
  exists n0 : nat,
    0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk

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

          rewrite INDNJ -subnDA addn1 -INDJ in INDSJ.

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

1 subgoal (ID 7942)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj, j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  n : nat
  NZN : 0 < n
  sj : Job
  ARR_IN_SJ : arrives_in arr_seq sj
  TSKSJ : job_task sj = tsk
  ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
  ARRJ'NJ : job_arrival j2 =
            job_arrival sj + task_period tsk + n * task_period tsk
  INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
  INDSJ : job_index arr_seq sj = job_index arr_seq j1
  ============================
  exists n0 : nat,
    0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk

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

          apply equal_index_implies_equal_jobs in INDSJ ⇒ //; last by rewrite TSKj1 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 7947)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj, j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  n : nat
  NZN : 0 < n
  sj : Job
  ARR_IN_SJ : arrives_in arr_seq sj
  TSKSJ : job_task sj = tsk
  ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
  ARRJ'NJ : job_arrival j2 =
            job_arrival sj + task_period tsk + n * task_period tsk
  INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
  INDSJ : sj = j1
  ============================
  exists n0 : nat,
    0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk

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

          ∃ (n.+1); split; try by ssrlia.

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

1 subgoal (ID 8011)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj, j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  n : nat
  NZN : 0 < n
  sj : Job
  ARR_IN_SJ : arrives_in arr_seq sj
  TSKSJ : job_task sj = tsk
  ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
  ARRJ'NJ : job_arrival j2 =
            job_arrival sj + task_period tsk + n * task_period tsk
  INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
  INDSJ : sj = j1
  ============================
  job_arrival j2 = job_arrival j1 + succn n * task_period tsk

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

          rewrite INDSJ in ARRJ'NJ; rewrite mulSnr.

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

1 subgoal (ID 9130)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  k, s : nat
  j2, nj, j1 : Job
  TSKj1 : job_task j1 = tsk
  TSKj2 : job_task j2 = tsk
  STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ARRj2 : arrives_in arr_seq j2
  ARRj1 : arrives_in arr_seq j1
  NEQNJ : j2 <> nj
  ARRNJ : arrives_in arr_seq nj
  INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
  TSKNJ : job_task nj = tsk
  n : nat
  NZN : 0 < n
  sj : Job
  ARR_IN_SJ : arrives_in arr_seq sj
  TSKSJ : job_task sj = tsk
  ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
  INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
  INDSJ : sj = j1
  ARRJ'NJ : job_arrival j2 =
            job_arrival j1 + task_period tsk + n * task_period tsk
  ============================
  job_arrival j2 = job_arrival j1 + (n * task_period tsk + task_period tsk)

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

          now ssrlia.

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

No more subgoals.

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

      }

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

No more subgoals.

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

    Qed.

  End ArrivalSeparationWithGivenIndexDifference.

Consider any two _distinct_ jobs [j1] and [j2] of task [tsk] that stem from the arrival sequence.
  Variable j1 j2 : Job.
  Hypothesis H_j1_neq_j2: j1 ≠ j2.
  Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
  Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
  Hypothesis H_j1_of_task: job_task j1 = tsk.
  Hypothesis H_j2_of_task: job_task j2 = tsk.

Without loss of generality, we assume that job [j1] arrives before job [j2].
  Hypothesis H_j1_before_j2: job_arrival j1 ≤ job_arrival j2.

We generalize the above lemma to show that any two unequal jobs of task [tsk] are separated by a non-zero multiple of [task_period tsk].
  Lemma job_sep_periodic:
    ∃ n,
      n > 0 ∧
      job_arrival j2 = job_arrival j1 + n × task_period tsk.

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

1 subgoal (ID 370)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  ============================
  exists n : nat,
    0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk

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

  Proof.
    apply job_arrival_separation_when_index_diff_is_k with (k := (job_index arr_seq j2 - job_index arr_seq j1)); try done.

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

2 subgoals (ID 383)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  ============================
  job_index arr_seq j1 + (job_index arr_seq j2 - job_index arr_seq j1) =
  job_index arr_seq j2

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

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

    - apply subnKC.

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

2 subgoals (ID 431)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  ============================
  job_index arr_seq j1 <= job_index arr_seq j2

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

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

      move_neq_up IND.

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

2 subgoals (ID 459)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  IND : job_index arr_seq j2 < job_index arr_seq j1
  ============================
  False

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

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

      eapply lower_index_implies_earlier_arrival in IND; eauto with basic_facts.

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

2 subgoals (ID 467)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  IND : job_arrival j2 < job_arrival j1
  ============================
  False

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

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

      now move_neq_down IND.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 384)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  ============================
  job_arrival j1 < job_arrival j2

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


    - case: (boolP (job_index arr_seq j1 == job_index arr_seq j2)) ⇒ [/eqP EQ_IND|NEQ_IND].

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

2 subgoals (ID 912)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  EQ_IND : job_index arr_seq j1 = job_index arr_seq j2
  ============================
  job_arrival j1 < job_arrival j2

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

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

      + now apply equal_index_implies_equal_jobs in EQ_IND ⇒ //; rewrite H_j1_of_task.

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

1 subgoal (ID 911)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  NEQ_IND : job_index arr_seq j1 != job_index arr_seq j2
  ============================
  job_arrival j1 < job_arrival j2

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

      + move: NEQ_IND; rewrite neq_ltn ⇒ /orP [LT|LT].

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

2 subgoals (ID 1020)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  LT : job_index arr_seq j1 < job_index arr_seq j2
  ============================
  job_arrival j1 < job_arrival j2

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

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

        × now eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.

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

1 subgoal (ID 1021)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  LT : job_index arr_seq j2 < job_index arr_seq j1
  ============================
  job_arrival j1 < job_arrival j2

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

        × eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.

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

1 subgoal (ID 1124)
  
  Task : TaskType
  H : PeriodicModel Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : 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_periodic_model : respects_periodic_task_model arr_seq tsk
  H_valid_period : valid_period tsk
  j1, j2 : Job
  H_j1_neq_j2 : j1 <> j2
  H_j1_from_arr_seq : arrives_in arr_seq j1
  H_j2_from_arr_seq : arrives_in arr_seq j2
  H_j1_of_task : job_task j1 = tsk
  H_j2_of_task : job_task j2 = tsk
  H_j1_before_j2 : job_arrival j1 <= job_arrival j2
  LT : job_arrival j2 < job_arrival j1
  ============================
  job_arrival j1 < job_arrival j2

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

          now move_neq_down LT.

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

No more subgoals.

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

  Qed.

End JobArrivalSeparation.