Library prosa.analysis.facts.hyperperiod


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

Welcome to Coq 8.11.2 (June 2020)

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

Require Export prosa.analysis.definitions.hyperperiod.
Require Export prosa.analysis.facts.periodic.task_arrivals_size.
Require Export prosa.util.div_mod.

In this file we prove some simple properties of hyperperiods of periodic tasks.
Section Hyperperiod.

Consider any type of periodic tasks, ...
  Context {Task : TaskType} `{PeriodicModel Task}.

... any task set [ts], ...
  Variable ts : TaskSet Task.

... and any task [tsk] that belongs to this task set.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts: tsk \in ts.

A task set's hyperperiod is an integral multiple of each task's period in the task set.
  Lemma hyperperiod_int_mult_of_any_task:
    ∃ (k : nat),
      hyperperiod ts = k × task_period tsk.

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

1 subgoal (ID 343)
  
  Task : TaskType
  H : PeriodicModel Task
  ts : TaskSet Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  ============================
  exists k : nat, hyperperiod ts = k * task_period tsk

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

  Proof.
    apply lcm_seq_is_mult_of_all_ints.

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

1 subgoal (ID 344)
  
  Task : TaskType
  H : PeriodicModel Task
  ts : TaskSet Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  ============================
  task_period tsk \in [seq task_period i | i <- ts]

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

    apply map_f.

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

1 subgoal (ID 345)
  
  Task : TaskType
  H : PeriodicModel Task
  ts : TaskSet Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  ============================
  tsk \in ts

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

    now apply H_tsk_in_ts.

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

No more subgoals.

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

  Qed.

End Hyperperiod.

In this section we show a property of hyperperiod in context of task sets with valid periods.
Section ValidPeriodsImplyPositiveHP.

Consider any type of periodic tasks ...
  Context {Task : TaskType} `{PeriodicModel Task}.

... and any task set [ts] ...
  Variable ts : TaskSet Task.

... such that all tasks in [ts] have valid periods.
  Hypothesis H_valid_periods: valid_periods ts.

We show that the hyperperiod of task set [ts] is positive.
  Lemma valid_periods_imply_pos_hp:
    hyperperiod ts > 0.

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

1 subgoal (ID 336)
  
  Task : TaskType
  H : PeriodicModel Task
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  ============================
  0 < hyperperiod ts

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

  Proof.
    apply all_pos_implies_lcml_pos.

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

1 subgoal (ID 337)
  
  Task : TaskType
  H : PeriodicModel Task
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  ============================
  forall b : nat_eqType, b \in [seq task_period i | i <- ts] -> 0 < b

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

    move ⇒ b /mapP [x IN EQ]; subst b.

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

1 subgoal (ID 394)
  
  Task : TaskType
  H : PeriodicModel Task
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  x : Task
  IN : x \in ts
  ============================
  0 < task_period x

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

    now apply H_valid_periods.

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

No more subgoals.

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

  Qed.

End ValidPeriodsImplyPositiveHP.

In this section we prove some lemmas about the hyperperiod in context of the periodic model.
Section PeriodicLemmas.

Consider any type of tasks, ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.

... any type of jobs, ...
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

... and a consistent arrival sequence with non-duplicate 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.

Consider a task set [ts] such that all tasks in [ts] have valid periods.
  Variable ts : TaskSet Task.
  Hypothesis H_valid_periods: valid_periods ts.

Let [tsk] be any periodic task in [ts] with a valid offset and period.
  Variable tsk : Task.
  Hypothesis H_task_in_ts: tsk \in ts.
  Hypothesis H_valid_offset: valid_offset arr_seq tsk.
  Hypothesis H_valid_period: valid_period tsk.
  Hypothesis H_periodic_task: respects_periodic_task_model arr_seq tsk.

Assume we have an infinite sequence of jobs in the arrival sequence.
  Hypothesis H_infinite_jobs: infinite_jobs arr_seq.

Let [O_max] denote the maximum task offset in [ts] and let [HP] denote the hyperperiod of all tasks in [ts].
  Let O_max := max_task_offset ts.
  Let HP := hyperperiod ts.

We show that the job corresponding to any job [j1] in any other hyperperiod is of the same task as [j1].
  Lemma corresponding_jobs_have_same_task:
    ∀ j1 j2,
      job_task (corresponding_job_in_hyperperiod ts arr_seq j1
               (starting_instant_of_corresponding_hyperperiod ts j2) (job_task j1)) = job_task j1.

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

1 subgoal (ID 386)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  ============================
  forall j1 j2 : Job,
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

  Proof.
    intros ×.

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

1 subgoal (ID 388)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j1, j2 : Job
  ============================
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

    set ARRIVALS := (task_arrivals_between arr_seq (job_task j1) (starting_instant_of_hyperperiod ts (job_arrival j2))
          (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)).

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

1 subgoal (ID 406)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j1, j2 : Job
  ARRIVALS := task_arrivals_between arr_seq (job_task j1)
                (starting_instant_of_hyperperiod ts (job_arrival j2))
                (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)
   : seq Job
  ============================
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

    set IND := (job_index_in_hyperperiod ts arr_seq j1 (starting_instant_of_hyperperiod ts (job_arrival j1)) (job_task j1)).

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

1 subgoal (ID 420)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j1, j2 : Job
  ARRIVALS := task_arrivals_between arr_seq (job_task j1)
                (starting_instant_of_hyperperiod ts (job_arrival j2))
                (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)
   : seq Job
  IND := job_index_in_hyperperiod ts arr_seq j1
           (starting_instant_of_hyperperiod ts (job_arrival j1))
           (job_task j1) : nat
  ============================
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

    have SIZE_G : size ARRIVALS ≤ IND → job_task (nth j1 ARRIVALS IND) = job_task j1 by intro SG; rewrite nth_default.

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

1 subgoal (ID 442)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j1, j2 : Job
  ARRIVALS := task_arrivals_between arr_seq (job_task j1)
                (starting_instant_of_hyperperiod ts (job_arrival j2))
                (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)
   : seq Job
  IND := job_index_in_hyperperiod ts arr_seq j1
           (starting_instant_of_hyperperiod ts (job_arrival j1))
           (job_task j1) : nat
  SIZE_G : size ARRIVALS <= IND ->
           job_task (nth j1 ARRIVALS IND) = job_task j1
  ============================
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

    case: (boolP (size ARRIVALS == IND)) ⇒ [/eqP EQ|NEQ]; first by apply SIZE_G; ssrlia.

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

1 subgoal (ID 488)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j1, j2 : Job
  ARRIVALS := task_arrivals_between arr_seq (job_task j1)
                (starting_instant_of_hyperperiod ts (job_arrival j2))
                (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)
   : seq Job
  IND := job_index_in_hyperperiod ts arr_seq j1
           (starting_instant_of_hyperperiod ts (job_arrival j1))
           (job_task j1) : nat
  SIZE_G : size ARRIVALS <= IND ->
           job_task (nth j1 ARRIVALS IND) = job_task j1
  NEQ : size ARRIVALS != IND
  ============================
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

    move : NEQ; rewrite neq_ltn; move ⇒ /orP [LT | G]; first by apply SIZE_G; ssrlia.

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

1 subgoal (ID 838)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j1, j2 : Job
  ARRIVALS := task_arrivals_between arr_seq (job_task j1)
                (starting_instant_of_hyperperiod ts (job_arrival j2))
                (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)
   : seq Job
  IND := job_index_in_hyperperiod ts arr_seq j1
           (starting_instant_of_hyperperiod ts (job_arrival j1))
           (job_task j1) : nat
  SIZE_G : size ARRIVALS <= IND ->
           job_task (nth j1 ARRIVALS IND) = job_task j1
  G : IND < size ARRIVALS
  ============================
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

    set jb := nth j1 ARRIVALS IND.

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

1 subgoal (ID 1166)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j1, j2 : Job
  ARRIVALS := task_arrivals_between arr_seq (job_task j1)
                (starting_instant_of_hyperperiod ts (job_arrival j2))
                (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)
   : seq Job
  IND := job_index_in_hyperperiod ts arr_seq j1
           (starting_instant_of_hyperperiod ts (job_arrival j1))
           (job_task j1) : nat
  SIZE_G : size ARRIVALS <= IND ->
           job_task (nth j1 ARRIVALS IND) = job_task j1
  G : IND < size ARRIVALS
  jb := nth j1 ARRIVALS IND : Job
  ============================
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

    have JOB_IN : jb \in ARRIVALS by apply mem_nth.

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

1 subgoal (ID 1174)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j1, j2 : Job
  ARRIVALS := task_arrivals_between arr_seq (job_task j1)
                (starting_instant_of_hyperperiod ts (job_arrival j2))
                (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)
   : seq Job
  IND := job_index_in_hyperperiod ts arr_seq j1
           (starting_instant_of_hyperperiod ts (job_arrival j1))
           (job_task j1) : nat
  SIZE_G : size ARRIVALS <= IND ->
           job_task (nth j1 ARRIVALS IND) = job_task j1
  G : IND < size ARRIVALS
  jb := nth j1 ARRIVALS IND : Job
  JOB_IN : jb \in ARRIVALS
  ============================
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

    rewrite /ARRIVALS /task_arrivals_between mem_filter in JOB_IN.

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

1 subgoal (ID 1222)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j1, j2 : Job
  ARRIVALS := task_arrivals_between arr_seq (job_task j1)
                (starting_instant_of_hyperperiod ts (job_arrival j2))
                (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)
   : seq Job
  IND := job_index_in_hyperperiod ts arr_seq j1
           (starting_instant_of_hyperperiod ts (job_arrival j1))
           (job_task j1) : nat
  SIZE_G : size ARRIVALS <= IND ->
           job_task (nth j1 ARRIVALS IND) = job_task j1
  G : IND < size ARRIVALS
  jb := nth j1 ARRIVALS IND : Job
  JOB_IN : (job_task jb == job_task j1) &&
           (jb
              \in arrivals_between arr_seq
                    (starting_instant_of_hyperperiod ts (job_arrival j2))
                    (starting_instant_of_hyperperiod ts (job_arrival j2) + HP))
  ============================
  job_task
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) 
       (job_task j1)) = job_task j1

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

    now move : JOB_IN ⇒ /andP [/eqP TSK JB_IN].

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

No more subgoals.

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

  Qed.

We show that if a job [j] lies in the hyperperiod starting at instant [t] then [j] arrives in the interval [t, t + HP).
  Lemma all_jobs_arrive_within_hyperperiod:
    ∀ j t,
      j \in jobs_in_hyperperiod ts arr_seq t tsk→
      t ≤ job_arrival j < t + HP.

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

1 subgoal (ID 402)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  ============================
  forall (j : Job) (t : instant),
  j \in jobs_in_hyperperiod ts arr_seq t tsk -> t <= job_arrival j < t + HP

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

  Proof.
    intros × JB_IN_HP.

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

1 subgoal (ID 405)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j : Job
  t : instant
  JB_IN_HP : j \in jobs_in_hyperperiod ts arr_seq t tsk
  ============================
  t <= job_arrival j < t + HP

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

    rewrite mem_filter in JB_IN_HP.

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

1 subgoal (ID 440)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j : Job
  t : instant
  JB_IN_HP : (job_task j == tsk) &&
             (j \in arrivals_between arr_seq t (t + hyperperiod ts))
  ============================
  t <= job_arrival j < t + HP

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

    move : JB_IN_HP ⇒ /andP [/eqP TSK JB_IN]; apply mem_bigcat_nat_exists in JB_IN.

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

1 subgoal (ID 515)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j : Job
  t : instant
  TSK : job_task j = tsk
  JB_IN : exists i : nat,
            j \in arrivals_at arr_seq i /\ t <= i < t + hyperperiod ts
  ============================
  t <= job_arrival j < t + HP

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

    destruct JB_IN as [i [JB_IN INEQ]]; apply H_consistent_arrivals in JB_IN.

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

1 subgoal (ID 526)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  j : Job
  t : instant
  TSK : job_task j = tsk
  i : nat
  JB_IN : job_arrival j = i
  INEQ : t <= i < t + hyperperiod ts
  ============================
  t <= job_arrival j < t + HP

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

    now rewrite JB_IN.

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

No more subgoals.

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

  Qed.

We show that the number of jobs in a hyperperiod starting at [n1 * HP + O_max] is the same as the number of jobs in a hyperperiod starting at [n2 * HP + O_max] given that [n1] is less than or equal to [n2].
  Lemma eq_size_hyp_lt:
    ∀ n1 n2,
      n1 ≤ n2 →
      size (jobs_in_hyperperiod ts arr_seq (n1 × HP + O_max) tsk) =
      size (jobs_in_hyperperiod ts arr_seq (n2 × HP + O_max) tsk).

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

1 subgoal (ID 417)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  ============================
  forall n1 n2 : nat,
  n1 <= n2 ->
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

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

  Proof.
    intros × N1_LT.

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

1 subgoal (ID 420)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

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

    specialize (add_mul_diff n1 n2 HP O_max) ⇒ AD; feed_n 1 AD ⇒ //.

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

1 subgoal (ID 429)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  AD : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

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

    rewrite AD.

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

1 subgoal (ID 453)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  AD : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size
    (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max + (n2 - n1) * HP) tsk)

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

    destruct (hyperperiod_int_mult_of_any_task ts tsk H_task_in_ts) as [k HYP]; rewrite !/HP.

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

1 subgoal (ID 462)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  AD : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
  k : nat
  HYP : hyperperiod ts = k * task_period tsk
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * hyperperiod ts + O_max) tsk) =
  size
    (jobs_in_hyperperiod ts arr_seq
       (n1 * hyperperiod ts + O_max + (n2 - n1) * hyperperiod ts) tsk)

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

    rewrite [in X in _ = size (_ (n1 × HP + O_max + _ × X) tsk)]HYP.

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

1 subgoal (ID 486)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  AD : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
  k : nat
  HYP : hyperperiod ts = k * task_period tsk
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * hyperperiod ts + O_max) tsk) =
  size
    (jobs_in_hyperperiod ts arr_seq
       (n1 * HP + O_max + (n2 - n1) * (k * task_period tsk)) tsk)

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

    rewrite mulnA /HP /jobs_in_hyperperiod !size_of_task_arrivals_between.

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

1 subgoal (ID 524)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  AD : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
  k : nat
  HYP : hyperperiod ts = k * task_period tsk
  ============================
  \sum_(n1 * hyperperiod ts + O_max <= t < n1 * hyperperiod ts + O_max +
                                           hyperperiod ts)
     size (task_arrivals_at arr_seq tsk t) =
  \sum_(n1 * hyperperiod ts + O_max + (n2 - n1) * k * task_period tsk <= t < 
  n1 * hyperperiod ts + O_max + (n2 - n1) * k * task_period tsk +
  hyperperiod ts) size (task_arrivals_at arr_seq tsk t)

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

    erewrite big_sum_eq_in_eq_sized_intervals ⇒ //; intros g G_LT.

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

1 subgoal (ID 584)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  AD : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
  k : nat
  HYP : hyperperiod ts = k * task_period tsk
  g : nat
  G_LT : g < hyperperiod ts
  ============================
  size (task_arrivals_at arr_seq tsk (n1 * hyperperiod ts + O_max + g)) =
  (fun t : nat => size (task_arrivals_at arr_seq tsk t))
    (n1 * hyperperiod ts + O_max + (n2 - n1) * k * task_period tsk + g)

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

    have OFF_G : task_offset tsk ≤ O_max by apply max_offset_g.

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

1 subgoal (ID 592)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  AD : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
  k : nat
  HYP : hyperperiod ts = k * task_period tsk
  g : nat
  G_LT : g < hyperperiod ts
  OFF_G : task_offset tsk <= O_max
  ============================
  size (task_arrivals_at arr_seq tsk (n1 * hyperperiod ts + O_max + g)) =
  size
    (task_arrivals_at arr_seq tsk
       (n1 * hyperperiod ts + O_max + (n2 - n1) * k * task_period tsk + g))

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

    have FG : ∀ v b n, v + b + n = v + n + b by intros *; ssrlia.

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

1 subgoal (ID 1081)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  AD : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
  k : nat
  HYP : hyperperiod ts = k * task_period tsk
  g : nat
  G_LT : g < hyperperiod ts
  OFF_G : task_offset tsk <= O_max
  FG : forall v b n : nat, v + b + n = v + n + b
  ============================
  size (task_arrivals_at arr_seq tsk (n1 * hyperperiod ts + O_max + g)) =
  size
    (task_arrivals_at arr_seq tsk
       (n1 * hyperperiod ts + O_max + (n2 - n1) * k * task_period tsk + g))

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

    erewrite eq_size_of_task_arrivals_seperated_by_period ⇒ //; last by ssrlia.

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

1 focused subgoal
(shelved: 1) (ID 1089)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  N1_LT : n1 <= n2
  AD : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP
  k : nat
  HYP : hyperperiod ts = k * task_period tsk
  g : nat
  G_LT : g < hyperperiod ts
  OFF_G : task_offset tsk <= O_max
  FG : forall v b n : nat, v + b + n = v + n + b
  ============================
  size
    (task_arrivals_at arr_seq tsk
       (n1 * hyperperiod ts + O_max + g + ?n * task_period tsk)) =
  size
    (task_arrivals_at arr_seq tsk
       (n1 * hyperperiod ts + O_max + (n2 - n1) * k * task_period tsk + g))

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

    now rewrite FG.

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

No more subgoals.

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

  Qed.

We generalize the above lemma by lifting the condition on [n1] and [n2].
  Lemma eq_size_of_arrivals_in_hyperperiod:
    ∀ n1 n2,
      size (jobs_in_hyperperiod ts arr_seq (n1 × HP + O_max) tsk) =
      size (jobs_in_hyperperiod ts arr_seq (n2 × HP + O_max) tsk).

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

1 subgoal (ID 432)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  ============================
  forall n1 n2 : nat,
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

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

  Proof.
    intros ×.

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

1 subgoal (ID 434)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

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

    case : (boolP (n1 == n2)) ⇒ [/eqP EQ | NEQ]; first by rewrite EQ.

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

1 subgoal (ID 479)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  NEQ : n1 != n2
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

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

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

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

2 subgoals (ID 531)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  LT : n1 < n2
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

subgoal 2 (ID 532) is:
 size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
 size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

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

    + now apply eq_size_hyp_lt ⇒ //; ssrlia.

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

1 subgoal (ID 532)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  LT : n2 < n1
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

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

    + move : (eq_size_hyp_lt n2 n1) ⇒ EQ_S.

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

1 subgoal (ID 740)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  n1, n2 : nat
  LT : n2 < n1
  EQ_S : n2 <= n1 ->
         size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk) =
         size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk)
  ============================
  size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
  size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk)

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

      now feed_n 1 EQ_S ⇒ //; ssrlia.

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

No more subgoals.

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

  Qed.

Consider any two jobs [j1] and [j2] that stem from the arrival sequence [arr_seq] such that [j1] is 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_task: job_task j1 = tsk.

Assume that both [j1] and [j2] arrive after [O_max].
  Hypothesis H_j1_arr_after_O_max: O_max ≤ job_arrival j1.
  Hypothesis H_j2_arr_after_O_max: O_max ≤ job_arrival j2.

We show that any job [j] that arrives in task arrivals in the same hyperperiod as [j2] also arrives in task arrivals up to [job_arrival j2 + HP].
  Lemma job_in_hp_arrives_in_task_arrivals_up_to:
    ∀ j,
      j \in jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP × HP + O_max) tsk →
      j \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).

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

1 subgoal (ID 465)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  forall j : Job,
  j
    \in jobs_in_hyperperiod ts arr_seq
          ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk ->
  j \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP)

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

  Proof.
    intros j J_IN.

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

1 subgoal (ID 467)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : j
           \in jobs_in_hyperperiod ts arr_seq
                 ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk
  ============================
  j \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP)

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

    rewrite /task_arrivals_up_to.

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

1 subgoal (ID 474)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : j
           \in jobs_in_hyperperiod ts arr_seq
                 ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk
  ============================
  j \in task_arrivals_between arr_seq tsk 0 (succn (job_arrival j2 + HP))

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

    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP × HP + O_max) tsk).

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

1 subgoal (ID 482)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : j
           \in jobs_in_hyperperiod ts arr_seq
                 ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  ============================
  j \in task_arrivals_between arr_seq tsk 0 (succn (job_arrival j2 + HP))

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

    move : (J_IN) ⇒ J_ARR; apply all_jobs_arrive_within_hyperperiod in J_IN.

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

1 subgoal (ID 485)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  J_ARR : j
            \in jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk
  ============================
  j \in task_arrivals_between arr_seq tsk 0 (succn (job_arrival j2 + HP))

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

    rewrite /jobs_in_hp /jobs_in_hyperperiod /task_arrivals_up_to /task_arrivals_between mem_filter in J_ARR.

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

1 subgoal (ID 553)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  J_ARR : (job_task j == tsk) &&
          (j
             \in arrivals_between arr_seq
                   ((job_arrival j2 - O_max) %/ HP * HP + O_max)
                   ((job_arrival j2 - O_max) %/ HP * HP + O_max +
                    hyperperiod ts))
  ============================
  j \in task_arrivals_between arr_seq tsk 0 (succn (job_arrival j2 + HP))

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

    move : J_ARR ⇒ /andP [/eqP TSK' NTH_IN].

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

1 subgoal (ID 627)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  NTH_IN : j
             \in arrivals_between arr_seq
                   ((job_arrival j2 - O_max) %/ HP * HP + O_max)
                   ((job_arrival j2 - O_max) %/ HP * HP + O_max +
                    hyperperiod ts)
  ============================
  j \in task_arrivals_between arr_seq tsk 0 (succn (job_arrival j2 + HP))

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

    apply job_in_task_arrivals_between ⇒ //; first by apply in_arrivals_implies_arrived in NTH_IN.

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

1 subgoal (ID 635)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  NTH_IN : j
             \in arrivals_between arr_seq
                   ((job_arrival j2 - O_max) %/ HP * HP + O_max)
                   ((job_arrival j2 - O_max) %/ HP * HP + O_max +
                    hyperperiod ts)
  ============================
  0 <= job_arrival j < succn (job_arrival j2 + HP)

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

    apply mem_bigcat_nat_exists in NTH_IN.

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

1 subgoal (ID 688)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  NTH_IN : exists i : nat,
             j \in arrivals_at arr_seq i /\
             (job_arrival j2 - O_max) %/ HP * HP + O_max <= i <
             (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts
  ============================
  0 <= job_arrival j < succn (job_arrival j2 + HP)

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

    move : NTH_IN ⇒ [i [NJ_IN INEQ]]; apply H_consistent_arrivals in NJ_IN; rewrite -NJ_IN in INEQ.

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

1 subgoal (ID 756)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  i : nat
  NJ_IN : job_arrival j = i
  INEQ : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j <
         (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts
  ============================
  0 <= job_arrival j < succn (job_arrival j2 + HP)

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

    apply /andP; split ⇒ //.

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

1 subgoal (ID 783)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  i : nat
  NJ_IN : job_arrival j = i
  INEQ : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j <
         (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts
  ============================
  job_arrival j < succn (job_arrival j2 + HP)

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

    rewrite ltnS.

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

1 subgoal (ID 809)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  i : nat
  NJ_IN : job_arrival j = i
  INEQ : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j <
         (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts
  ============================
  job_arrival j <= job_arrival j2 + HP

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

    apply leq_trans with (n := (job_arrival j2 - O_max) %/ HP × HP + O_max + HP); first by ssrlia.

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

1 subgoal (ID 813)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  i : nat
  NJ_IN : job_arrival j = i
  INEQ : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j <
         (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts
  ============================
  (job_arrival j2 - O_max) %/ HP * HP + O_max + HP <= job_arrival j2 + HP

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

    rewrite leq_add2r.

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

1 subgoal (ID 2438)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  i : nat
  NJ_IN : job_arrival j = i
  INEQ : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j <
         (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts
  ============================
  (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j2

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

    have O_M : (job_arrival j2 - O_max) %/ HP × HP ≤ job_arrival j2 - O_max by apply leq_trunc_div.

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

1 subgoal (ID 2445)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  i : nat
  NJ_IN : job_arrival j = i
  INEQ : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j <
         (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts
  O_M : (job_arrival j2 - O_max) %/ HP * HP <= job_arrival j2 - O_max
  ============================
  (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j2

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

    have ARR_G : job_arrival j2 ≥ O_max by auto.

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

1 subgoal (ID 2450)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  j : Job
  J_IN : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j < (job_arrival j2 - O_max) %/ HP * HP + O_max + HP
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  TSK' : job_task j = tsk
  i : nat
  NJ_IN : job_arrival j = i
  INEQ : (job_arrival j2 - O_max) %/ HP * HP + O_max <= 
         job_arrival j <
         (job_arrival j2 - O_max) %/ HP * HP + O_max + hyperperiod ts
  O_M : (job_arrival j2 - O_max) %/ HP * HP <= job_arrival j2 - O_max
  ARR_G : O_max <= job_arrival j2
  ============================
  (job_arrival j2 - O_max) %/ HP * HP + O_max <= job_arrival j2

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

    now ssrlia.

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

No more subgoals.

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

  Qed.

We show that job [j1] arrives in its own hyperperiod.
  Lemma job_in_own_hp:
    j1 \in jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP × HP + O_max) tsk.

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

1 subgoal (ID 476)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  j1
    \in jobs_in_hyperperiod ts arr_seq
          ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk

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

  Proof.
    apply job_in_task_arrivals_between ⇒ //.

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

1 subgoal (ID 484)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  (job_arrival j1 - O_max) %/ HP * HP + O_max <= job_arrival j1 <
  (job_arrival j1 - O_max) %/ HP * HP + O_max + hyperperiod ts

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

    apply /andP; split.

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

2 subgoals (ID 532)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  (job_arrival j1 - O_max) %/ HP * HP + O_max <= job_arrival j1

subgoal 2 (ID 533) is:
 job_arrival j1 <
 (job_arrival j1 - O_max) %/ HP * HP + O_max + hyperperiod ts

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

    + rewrite addnC -leq_subRL ⇒ //.

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

2 subgoals (ID 545)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  (job_arrival j1 - O_max) %/ HP * HP <= job_arrival j1 - O_max

subgoal 2 (ID 533) is:
 job_arrival j1 <
 (job_arrival j1 - O_max) %/ HP * HP + O_max + hyperperiod ts

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

      now apply leq_trunc_div.

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

1 subgoal (ID 533)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  job_arrival j1 <
  (job_arrival j1 - O_max) %/ HP * HP + O_max + hyperperiod ts

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

    + specialize (div_floor_add_g (job_arrival j1 - O_max) HP) ⇒ AB.

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

1 subgoal (ID 573)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  AB : 0 < HP ->
       job_arrival j1 - O_max < (job_arrival j1 - O_max) %/ HP * HP + HP
  ============================
  job_arrival j1 <
  (job_arrival j1 - O_max) %/ HP * HP + O_max + hyperperiod ts

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

      feed_n 1 AB; first by apply valid_periods_imply_pos_hp ⇒ //.

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

1 subgoal (ID 579)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  AB : job_arrival j1 - O_max < (job_arrival j1 - O_max) %/ HP * HP + HP
  ============================
  job_arrival j1 <
  (job_arrival j1 - O_max) %/ HP * HP + O_max + hyperperiod ts

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

      apply ltn_subLR in AB.

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

1 subgoal (ID 583)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  AB : job_arrival j1 < (job_arrival j1 - O_max) %/ HP * HP + HP + O_max
  ============================
  job_arrival j1 <
  (job_arrival j1 - O_max) %/ HP * HP + O_max + hyperperiod ts

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

      now rewrite -/(HP); ssrlia.

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

No more subgoals.

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

  Qed.

We show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod arrives in task arrivals up to [job_arrival j2 + HP].
  Lemma corr_job_in_task_arrivals_up_to:
    corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk \in
      task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).

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

1 subgoal (ID 497)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  corresponding_job_in_hyperperiod ts arr_seq j1
    (starting_instant_of_corresponding_hyperperiod ts j2) tsk
    \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP)

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

  Proof.
    rewrite /corresponding_job_in_hyperperiod /starting_instant_of_corresponding_hyperperiod.

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

1 subgoal (ID 521)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  nth j1
    (jobs_in_hyperperiod ts arr_seq
       (starting_instant_of_hyperperiod ts (job_arrival j2)) tsk)
    (job_index_in_hyperperiod ts arr_seq j1
       (starting_instant_of_hyperperiod ts (job_arrival j1)) tsk)
    \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP)

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

    rewrite /job_index_in_hyperperiod /starting_instant_of_hyperperiod /hyperperiod_index.

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

1 subgoal (ID 544)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  nth j1
    (jobs_in_hyperperiod ts arr_seq
       ((job_arrival j2 - max_task_offset ts) %/ hyperperiod ts *
        hyperperiod ts + max_task_offset ts) tsk)
    (index j1
       (jobs_in_hyperperiod ts arr_seq
          ((job_arrival j1 - max_task_offset ts) %/ hyperperiod ts *
           hyperperiod ts + max_task_offset ts) tsk))
    \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP)

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

    set ind := (index j1 (jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP × HP + O_max) tsk)).

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

1 subgoal (ID 553)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ind := index j1
           (jobs_in_hyperperiod ts arr_seq
              ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk) : nat
  ============================
  nth j1
    (jobs_in_hyperperiod ts arr_seq
       ((job_arrival j2 - max_task_offset ts) %/ hyperperiod ts *
        hyperperiod ts + max_task_offset ts) tsk) ind
    \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP)

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

    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP × HP + O_max) tsk).

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

1 subgoal (ID 561)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ind := index j1
           (jobs_in_hyperperiod ts arr_seq
              ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk) : nat
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  ============================
  nth j1 jobs_in_hp ind
    \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP)

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

    set nj := nth j1 jobs_in_hp ind.

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

1 subgoal (ID 564)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ind := index j1
           (jobs_in_hyperperiod ts arr_seq
              ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk) : nat
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  nj := nth j1 jobs_in_hp ind : Job
  ============================
  nj \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP)

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

    apply job_in_hp_arrives_in_task_arrivals_up_to ⇒ //.

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

1 subgoal (ID 565)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ind := index j1
           (jobs_in_hyperperiod ts arr_seq
              ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk) : nat
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  nj := nth j1 jobs_in_hp ind : Job
  ============================
  nj
    \in jobs_in_hyperperiod ts arr_seq
          ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk

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

    rewrite mem_nth /jobs_in_hp ⇒ //.

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

1 subgoal (ID 597)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ind := index j1
           (jobs_in_hyperperiod ts arr_seq
              ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk) : nat
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  nj := nth j1 jobs_in_hp ind : Job
  ============================
  ind <
  size
    (jobs_in_hyperperiod ts arr_seq
       ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk)

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

    specialize (eq_size_of_arrivals_in_hyperperiod ((job_arrival j2 - O_max) %/ HP) ((job_arrival j1 - O_max) %/ HP)) ⇒ EQ.

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

1 subgoal (ID 626)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ind := index j1
           (jobs_in_hyperperiod ts arr_seq
              ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk) : nat
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  nj := nth j1 jobs_in_hp ind : Job
  EQ : size
         (jobs_in_hyperperiod ts arr_seq
            ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk) =
       size
         (jobs_in_hyperperiod ts arr_seq
            ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk)
  ============================
  ind <
  size
    (jobs_in_hyperperiod ts arr_seq
       ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk)

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

    rewrite EQ /ind index_mem.

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

1 subgoal (ID 634)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ind := index j1
           (jobs_in_hyperperiod ts arr_seq
              ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk) : nat
  jobs_in_hp := jobs_in_hyperperiod ts arr_seq
                  ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk : 
  seq Job
  nj := nth j1 jobs_in_hp ind : Job
  EQ : size
         (jobs_in_hyperperiod ts arr_seq
            ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk) =
       size
         (jobs_in_hyperperiod ts arr_seq
            ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk)
  ============================
  j1
    \in jobs_in_hyperperiod ts arr_seq
          ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk

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

    now apply job_in_own_hp.

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

No more subgoals.

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

  Qed.

Finally, we show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod arrives in the arrival sequence [arr_seq].
  Lemma corresponding_job_arrives:
      arrives_in arr_seq (corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk).

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

1 subgoal (ID 510)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ============================
  arrives_in arr_seq
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) tsk)

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

  Proof.
    move : (corr_job_in_task_arrivals_up_to) ⇒ ARR_G.

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

1 subgoal (ID 512)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ARR_G : corresponding_job_in_hyperperiod ts arr_seq j1
            (starting_instant_of_corresponding_hyperperiod ts j2) tsk
            \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP)
  ============================
  arrives_in arr_seq
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) tsk)

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

    rewrite /task_arrivals_up_to /task_arrivals_between mem_filter in ARR_G.

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

1 subgoal (ID 566)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  ARR_G : (job_task
             (corresponding_job_in_hyperperiod ts arr_seq j1
                (starting_instant_of_corresponding_hyperperiod ts j2) tsk) ==
           tsk) &&
          (corresponding_job_in_hyperperiod ts arr_seq j1
             (starting_instant_of_corresponding_hyperperiod ts j2) tsk
             \in arrivals_between arr_seq 0 (succn (job_arrival j2 + HP)))
  ============================
  arrives_in arr_seq
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) tsk)

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

    move : ARR_G ⇒ /andP [/eqP TSK' NTH_IN].

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

1 subgoal (ID 640)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  ts : TaskSet Task
  H_valid_periods : valid_periods ts
  tsk : Task
  H_task_in_ts : tsk \in ts
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_periodic_task : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  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_task : job_task j1 = tsk
  H_j1_arr_after_O_max : O_max <= job_arrival j1
  H_j2_arr_after_O_max : O_max <= job_arrival j2
  TSK' : job_task
           (corresponding_job_in_hyperperiod ts arr_seq j1
              (starting_instant_of_corresponding_hyperperiod ts j2) tsk) =
         tsk
  NTH_IN : corresponding_job_in_hyperperiod ts arr_seq j1
             (starting_instant_of_corresponding_hyperperiod ts j2) tsk
             \in arrivals_between arr_seq 0 (succn (job_arrival j2 + HP))
  ============================
  arrives_in arr_seq
    (corresponding_job_in_hyperperiod ts arr_seq j1
       (starting_instant_of_corresponding_hyperperiod ts j2) tsk)

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

    now apply in_arrivals_implies_arrived in NTH_IN.

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

No more subgoals.

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

  Qed.

End PeriodicLemmas.