Library prosa.analysis.facts.periodic.task_arrivals_size


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

Welcome to Coq 8.13.0 (January 2021)

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

Require Export prosa.analysis.facts.periodic.arrival_times.
Require Export prosa.analysis.definitions.infinite_jobs.

In this file we prove some properties concerning the size of task arrivals in context of the periodic model.
Section TaskArrivalsSize.

Consider any type of periodic tasks with an offset ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.

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

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

... and any periodic task [tsk] with a valid offset and period.
  Variable tsk : Task.
  Hypothesis H_valid_offset: valid_offset arr_seq tsk.
  Hypothesis H_valid_period: valid_period tsk.
  Hypothesis H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk.

We show that if an instant [t] is not an "arrival time" for task [tsk] then [task_arrivals_at arr_seq tsk t] is an empty sequence.
  Lemma task_arrivals_size_at_non_arrival:
    ∀ t,
      (∀ n, t ≠ task_offset tsk + n × task_period tsk) →
      task_arrivals_at arr_seq tsk t = [::].

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

1 subgoal (ID 46)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  ============================
  forall t : nat,
  (forall n : nat, t <> task_offset tsk + n * task_period tsk) ->
  task_arrivals_at arr_seq tsk t = [::]

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

  Proof.
    intros × T.

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

1 subgoal (ID 48)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  ============================
  task_arrivals_at arr_seq tsk t = [::]

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

    have EMPT_OR_EXISTS : ∀ xs, xs = [::] ∨ ∃ a, a \in xs.

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

2 subgoals (ID 62)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  ============================
  forall (t0 : eqType) (xs : seq t0), xs = [::] \/ (exists a : t0, a \in xs)

subgoal 2 (ID 64) is:
 task_arrivals_at arr_seq tsk t = [::]

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

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

1 subgoal (ID 62)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  ============================
  forall (t0 : eqType) (xs : seq t0), xs = [::] \/ (exists a : t0, a \in xs)

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

intros ×.

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

1 subgoal (ID 66)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  t0 : eqType
  xs : seq t0
  ============================
  xs = [::] \/ (exists a : t0, a \in xs)

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

      induction xs; first by left.

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

1 subgoal (ID 74)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  t0 : eqType
  a : t0
  xs : seq t0
  IHxs : xs = [::] \/ (exists a : t0, a \in xs)
  ============================
  a :: xs = [::] \/ (exists a0 : t0, a0 \in a :: xs)

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

      right; ∃ a.

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

1 subgoal (ID 80)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  t0 : eqType
  a : t0
  xs : seq t0
  IHxs : xs = [::] \/ (exists a : t0, a \in xs)
  ============================
  a \in a :: xs

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

      now apply mem_head.

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

1 subgoal

subgoal 1 (ID 64) is:
 task_arrivals_at arr_seq tsk t = [::]

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

    }

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

1 subgoal (ID 64)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
                   xs = [::] \/ (exists a : t, a \in xs)
  ============================
  task_arrivals_at arr_seq tsk t = [::]

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

    destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] ⇒ //.

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

1 subgoal (ID 95)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
                   xs = [::] \/ (exists a : t, a \in xs)
  a : Job
  A_IN : a \in task_arrivals_at arr_seq tsk t
  ============================
  task_arrivals_at arr_seq tsk t = [::]

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

    rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN ⇒ /andP [/eqP TSK A_ARR].

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

1 subgoal (ID 226)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
                   xs = [::] \/ (exists a : t, a \in xs)
  a : Job
  TSK : job_task a = tsk
  A_ARR : a \in arrivals_at arr_seq t
  ============================
  task_arrivals_at arr_seq tsk t = [::]

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

    move : (A_ARR) ⇒ A_IN; apply H_consistent_arrivals in A_IN.

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

1 subgoal (ID 230)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  T : forall n : nat, t <> task_offset tsk + n * task_period tsk
  EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
                   xs = [::] \/ (exists a : t, a \in xs)
  a : Job
  TSK : job_task a = tsk
  A_ARR : a \in arrivals_at arr_seq t
  A_IN : job_arrival a = t
  ============================
  task_arrivals_at arr_seq tsk t = [::]

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

    rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.

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

1 subgoal (ID 289)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
                   xs = [::] \/ (exists a : t, a \in xs)
  a : Job
  TSK : job_task a = tsk
  A_IN : job_arrival a = t
  T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
  A_ARR : a \in arr_seq t
  ============================
  task_arrivals_at arr_seq tsk t = [::]

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

    apply in_arrseq_implies_arrives in A_ARR.

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

1 subgoal (ID 292)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
                   xs = [::] \/ (exists a : t, a \in xs)
  a : Job
  TSK : job_task a = tsk
  A_IN : job_arrival a = t
  T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
  A_ARR : arrives_in arr_seq a
  ============================
  task_arrivals_at arr_seq tsk t = [::]

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

    have EXISTS_N : ∃ n, job_arrival a = task_offset tsk + n × task_period tsk by
          apply job_arrival_times with (arr_seq0 := arr_seq) ⇒ //.

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

1 subgoal (ID 316)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
                   xs = [::] \/ (exists a : t, a \in xs)
  a : Job
  TSK : job_task a = tsk
  A_IN : job_arrival a = t
  T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
  A_ARR : arrives_in arr_seq a
  EXISTS_N : exists n : nat,
               job_arrival a = task_offset tsk + n * task_period tsk
  ============================
  task_arrivals_at arr_seq tsk t = [::]

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

    move : EXISTS_N ⇒ [n A_ARRIVAL].

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

1 subgoal (ID 329)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : nat
  EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
                   xs = [::] \/ (exists a : t, a \in xs)
  a : Job
  TSK : job_task a = tsk
  A_IN : job_arrival a = t
  T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
  A_ARR : arrives_in arr_seq a
  n : nat
  A_ARRIVAL : job_arrival a = task_offset tsk + n * task_period tsk
  ============================
  task_arrivals_at arr_seq tsk t = [::]

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

    now move : (T n) ⇒ T1.

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

No more subgoals.

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

  Qed.

We show that at any instant [t], at most one job of task [tsk] can arrive (i.e. size of [task_arrivals_at arr_seq tsk t] is at most one).
  Lemma task_arrivals_at_size_cases:
    ∀ t,
      size (task_arrivals_at arr_seq tsk t) = 0 ∨
      size (task_arrivals_at arr_seq tsk t) = 1.

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

1 subgoal (ID 58)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  ============================
  forall t : instant,
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

  Proof.
    intro t.

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

1 subgoal (ID 59)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) ⇒ [LT|GT|EQ]; try by auto.

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

2 subgoals (ID 119)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  LT : size (task_arrivals_at arr_seq tsk t) < 1
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

subgoal 2 (ID 120) is:
 size (task_arrivals_at arr_seq tsk t) = 0 \/
 size (task_arrivals_at arr_seq tsk t) = 1

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

    destruct (size (task_arrivals_at arr_seq tsk t)); now left.

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

1 subgoal (ID 120)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    specialize (exists_two Job (task_arrivals_at arr_seq tsk t)) ⇒ EXISTS_TWO.

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

1 subgoal (ID 224)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  EXISTS_TWO : 1 < size (task_arrivals_at arr_seq tsk t) ->
               uniq (task_arrivals_at arr_seq tsk t) ->
               exists a b : Job,
                 a <> b /\
                 a \in task_arrivals_at arr_seq tsk t /\
                 b \in task_arrivals_at arr_seq tsk t
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

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

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

1 subgoal (ID 249)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  A_IN : a \in task_arrivals_at arr_seq tsk t
  B_IN : b \in task_arrivals_at arr_seq tsk t
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.

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

1 subgoal (ID 316)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  A_IN : (job_task a == tsk) && (a \in arrivals_at arr_seq t)
  B_IN : (job_task b == tsk) && (b \in arrivals_at arr_seq t)
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

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

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

1 subgoal (ID 459)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

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

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

1 subgoal (ID 466)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  A_IN : b \in arr_seq t
  B_IN : a \in arr_seq t
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.

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

1 subgoal (ID 472)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  A_IN : arrives_in arr_seq b
  B_IN : arrives_in arr_seq a
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    have SPO : respects_sporadic_task_model arr_seq tsk; try by auto with basic_facts.

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

1 subgoal (ID 481)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  A_IN : arrives_in arr_seq b
  B_IN : arrives_in arr_seq a
  SPO : respects_sporadic_task_model arr_seq tsk
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

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

(* ----------------------------------[ 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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  A_IN : arrives_in arr_seq b
  B_IN : arrives_in arr_seq a
  SPO : respects_sporadic_task_model arr_seq tsk
  EQ_ARR_A : job_arrival a = t
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

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

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

1 subgoal (ID 551)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  A_IN : arrives_in arr_seq b
  B_IN : arrives_in arr_seq a
  SPO : respects_sporadic_task_model arr_seq tsk
  EQ_ARR_A : job_arrival a = t
  EQ_ARR_B : job_arrival b = t
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    specialize (SPO a b); feed_n 6 SPO ⇒ //; try by ssrlia.

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

1 subgoal (ID 589)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  A_IN : arrives_in arr_seq b
  B_IN : arrives_in arr_seq a
  SPO : job_arrival a + task_min_inter_arrival_time tsk <= job_arrival b
  EQ_ARR_A : job_arrival a = t
  EQ_ARR_B : job_arrival b = t
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    rewrite EQ_ARR_A EQ_ARR_B in SPO.

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

1 subgoal (ID 1656)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  A_IN : arrives_in arr_seq b
  B_IN : arrives_in arr_seq a
  EQ_ARR_A : job_arrival a = t
  EQ_ARR_B : job_arrival b = t
  SPO : t + task_min_inter_arrival_time tsk <= t
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    rewrite /task_min_inter_arrival_time /periodic_as_sporadic in SPO.

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

1 subgoal (ID 1700)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  A_IN : arrives_in arr_seq b
  B_IN : arrives_in arr_seq a
  EQ_ARR_A : job_arrival a = t
  EQ_ARR_B : job_arrival b = t
  SPO : t + task_period tsk <= t
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    have POS : task_period tsk > 0 by auto.

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

1 subgoal (ID 1705)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  t : instant
  GT : 1 < size (task_arrivals_at arr_seq tsk t)
  a, b : Job
  NEQ : a <> b
  TSKA : job_task a = tsk
  ARRA : a \in arrivals_at arr_seq t
  TSKB : job_task b = tsk
  ARRB : b \in arrivals_at arr_seq t
  A_IN : arrives_in arr_seq b
  B_IN : arrives_in arr_seq a
  EQ_ARR_A : job_arrival a = t
  EQ_ARR_B : job_arrival b = t
  SPO : t + task_period tsk <= t
  POS : 0 < task_period tsk
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0 \/
  size (task_arrivals_at arr_seq tsk t) = 1

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

    now ssrlia.

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

No more subgoals.

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

  Qed.

We show that the size of task arrivals (strictly) between two consecutive arrival times is zero.
  Lemma size_task_arrivals_between_eq0:
    ∀ n,
      let l := (task_offset tsk + n × task_period tsk).+1 in
      let r := (task_offset tsk + n.+1 × task_period tsk) in
      size (task_arrivals_between arr_seq tsk l r) = 0.

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

1 subgoal (ID 73)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  ============================
  forall n : nat,
  let l := (task_offset tsk + n * task_period tsk).+1 in
  let r := task_offset tsk + n.+1 * task_period tsk in
  size (task_arrivals_between arr_seq tsk l r) = 0

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

  Proof.
    intros n l r; rewrite /l /r.

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

1 subgoal (ID 78)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  l := (task_offset tsk + n * task_period tsk).+1 : nat
  r := task_offset tsk + n.+1 * task_period tsk : nat
  ============================
  size
    (task_arrivals_between arr_seq tsk
       (task_offset tsk + n * task_period tsk).+1
       (task_offset tsk + n.+1 * task_period tsk)) = 0

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

    rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t INEQ.

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

1 subgoal (ID 129)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  l := (task_offset tsk + n * task_period tsk).+1 : nat
  r := task_offset tsk + n.+1 * task_period tsk : nat
  t : nat
  INEQ : task_offset tsk + n * task_period tsk < t <
         task_offset tsk + n.+1 * task_period tsk
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0

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

    rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n1 EQ.

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

1 subgoal (ID 166)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  l := (task_offset tsk + n * task_period tsk).+1 : nat
  r := task_offset tsk + n.+1 * task_period tsk : nat
  t : nat
  INEQ : task_offset tsk + n * task_period tsk < t <
         task_offset tsk + n.+1 * task_period tsk
  n1 : nat
  EQ : t = task_offset tsk + n1 * task_period tsk
  ============================
  False

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

    rewrite EQ in INEQ.

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

1 subgoal (ID 195)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  l := (task_offset tsk + n * task_period tsk).+1 : nat
  r := task_offset tsk + n.+1 * task_period tsk : nat
  t, n1 : nat
  EQ : t = task_offset tsk + n1 * task_period tsk
  INEQ : task_offset tsk + n * task_period tsk <
         task_offset tsk + n1 * task_period tsk <
         task_offset tsk + n.+1 * task_period tsk
  ============================
  False

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

    move : INEQ ⇒ /andP [INEQ1 INEQ2].

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

1 subgoal (ID 236)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  l := (task_offset tsk + n * task_period tsk).+1 : nat
  r := task_offset tsk + n.+1 * task_period tsk : nat
  t, n1 : nat
  EQ : t = task_offset tsk + n1 * task_period tsk
  INEQ1 : task_offset tsk + n * task_period tsk <
          task_offset tsk + n1 * task_period tsk
  INEQ2 : task_offset tsk + n1 * task_period tsk <
          task_offset tsk + n.+1 * task_period tsk
  ============================
  False

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

    rewrite ltn_add2l ltn_mul2r in INEQ1; rewrite ltn_add2l ltn_mul2r in INEQ2.

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

1 subgoal (ID 312)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  l := (task_offset tsk + n * task_period tsk).+1 : nat
  r := task_offset tsk + n.+1 * task_period tsk : nat
  t, n1 : nat
  EQ : t = task_offset tsk + n1 * task_period tsk
  INEQ1 : (0 < task_period tsk) && (n < n1)
  INEQ2 : (0 < task_period tsk) && (n1 < n.+1)
  ============================
  False

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

    move : INEQ1 INEQ2 ⇒ /andP [A B] /andP [C D].

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

1 subgoal (ID 393)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  l := (task_offset tsk + n * task_period tsk).+1 : nat
  r := task_offset tsk + n.+1 * task_period tsk : nat
  t, n1 : nat
  EQ : t = task_offset tsk + n1 * task_period tsk
  A : 0 < task_period tsk
  B : n < n1
  C : 0 < task_period tsk
  D : n1 < n.+1
  ============================
  False

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

    now ssrlia.

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

No more subgoals.

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

  Qed.

In this section we show some properties of task arrivals in case of an infinite sequence of jobs.
  Section TaskArrivalsInCaseOfInfiniteJobs.

Assume that we have an infinite sequence of jobs.
    Hypothesis H_infinite_jobs: infinite_jobs arr_seq.

We show that for any number [n], there exists a job [j] of task [tsk] such that [job_index] of [j] is equal to [n] and [j] arrives at [task_offset tsk + n * task_period tsk].
    Lemma jobs_exists_later:
      ∀ n,
      ∃ j,
        arrives_in arr_seq j ∧
        job_task j = tsk ∧
        job_arrival j = task_offset tsk + n × task_period tsk ∧
        job_index arr_seq j = n.

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

1 subgoal (ID 98)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  ============================
  forall n : nat,
  exists j : Job,
    arrives_in arr_seq j /\
    job_task j = tsk /\
    job_arrival j = task_offset tsk + n * task_period tsk /\
    job_index arr_seq j = n

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

    Proof.
      intros ×.

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

1 subgoal (ID 99)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  ============================
  exists j : Job,
    arrives_in arr_seq j /\
    job_task j = tsk /\
    job_arrival j = task_offset tsk + n * task_period tsk /\
    job_index arr_seq j = n

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

      destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].

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

1 subgoal (ID 113)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  IND : job_index arr_seq j = n
  ============================
  exists j0 : Job,
    arrives_in arr_seq j0 /\
    job_task j0 = tsk /\
    job_arrival j0 = task_offset tsk + n * task_period tsk /\
    job_index arr_seq j0 = n

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

      ∃ j; repeat split ⇒ //.

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

1 subgoal (ID 243)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  IND : job_index arr_seq j = n
  ============================
  job_arrival j = task_offset tsk + n * task_period tsk

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

      now apply periodic_arrival_times with (arr_seq0 := arr_seq) ⇒ //.

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

No more subgoals.

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

    Qed.

We show that the size of task arrivals at any arrival time is equal to one.
    Lemma task_arrivals_at_size:
      ∀ n,
        let l := (task_offset tsk + n × task_period tsk) in
        size (task_arrivals_at arr_seq tsk l) = 1.

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

1 subgoal (ID 109)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  ============================
  forall n : nat,
  let l := task_offset tsk + n * task_period tsk in
  size (task_arrivals_at arr_seq tsk l) = 1

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

    Proof.
      intros n l; rewrite /l.

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

1 subgoal (ID 112)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  l := task_offset tsk + n * task_period tsk : nat
  ============================
  size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
  1

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

      move : (jobs_exists_later n) ⇒ [j' [ARR [TSK [ARRIVAL IND]]]].

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

1 subgoal (ID 154)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  l := task_offset tsk + n * task_period tsk : nat
  j' : Job
  ARR : arrives_in arr_seq j'
  TSK : job_task j' = tsk
  ARRIVAL : job_arrival j' = task_offset tsk + n * task_period tsk
  IND : job_index arr_seq j' = n
  ============================
  size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
  1

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

      apply only_j_in_task_arrivals_at_j with (tsk0 := tsk) in ARR ⇒ //; last by
          auto with basic_facts.

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

1 subgoal (ID 162)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  l := task_offset tsk + n * task_period tsk : nat
  j' : Job
  ARR : task_arrivals_at_job_arrival arr_seq j' = [:: j']
  TSK : job_task j' = tsk
  ARRIVAL : job_arrival j' = task_offset tsk + n * task_period tsk
  IND : job_index arr_seq j' = n
  ============================
  size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
  1

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

      rewrite /task_arrivals_at_job_arrival TSK in ARR.

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

1 subgoal (ID 266)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  l := task_offset tsk + n * task_period tsk : nat
  j' : Job
  TSK : job_task j' = tsk
  ARRIVAL : job_arrival j' = task_offset tsk + n * task_period tsk
  IND : job_index arr_seq j' = n
  ARR : task_arrivals_at arr_seq tsk (job_arrival j') = [:: j']
  ============================
  size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
  1

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

      now rewrite -ARRIVAL ARR.

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

No more subgoals.

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

    Qed.

We show that the size of task arrivals up to [task_offset tsk] is equal to one.
    Lemma size_task_arrivals_up_to_offset:
      size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1.

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

1 subgoal (ID 117)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  ============================
  size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1

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

    Proof.
      rewrite /task_arrivals_up_to.

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

1 subgoal (ID 124)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  ============================
  size (task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1) = 1

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

      specialize (task_arrivals_between_cat arr_seq tsk 0 (task_offset tsk) (task_offset tsk).+1) ⇒ CAT.

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

1 subgoal (ID 134)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  CAT : 0 <= task_offset tsk ->
        task_offset tsk <= (task_offset tsk).+1 ->
        task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
        task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
        task_arrivals_between arr_seq tsk (task_offset tsk)
          (task_offset tsk).+1
  ============================
  size (task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1) = 1

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

      feed_n 2 CAT ⇒ //; rewrite CAT size_cat.

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

1 subgoal (ID 174)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
        task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
        task_arrivals_between arr_seq tsk (task_offset tsk)
          (task_offset tsk).+1
  ============================
  size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
  size
    (task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
  1

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

      have Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0.

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

2 subgoals (ID 182)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
        task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
        task_arrivals_between arr_seq tsk (task_offset tsk)
          (task_offset tsk).+1
  ============================
  size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0

subgoal 2 (ID 184) is:
 size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
 size
   (task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
 1

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

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

1 subgoal (ID 182)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
        task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
        task_arrivals_between arr_seq tsk (task_offset tsk)
          (task_offset tsk).+1
  ============================
  size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0

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

rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t T_EQ.

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

1 subgoal (ID 235)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
        task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
        task_arrivals_between arr_seq tsk (task_offset tsk)
          (task_offset tsk).+1
  t : nat
  T_EQ : 0 <= t < task_offset tsk
  ============================
  size (task_arrivals_at arr_seq tsk t) = 0

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

        rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n EQ.

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

1 subgoal (ID 272)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
        task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
        task_arrivals_between arr_seq tsk (task_offset tsk)
          (task_offset tsk).+1
  t : nat
  T_EQ : 0 <= t < task_offset tsk
  n : nat
  EQ : t = task_offset tsk + n * task_period tsk
  ============================
  False

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

        now ssrlia.

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

1 subgoal

subgoal 1 (ID 184) is:
 size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
 size
   (task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
 1

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

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

1 subgoal (ID 184)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
        task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
        task_arrivals_between arr_seq tsk (task_offset tsk)
          (task_offset tsk).+1
  Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
  ============================
  size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
  size
    (task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
  1

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

              
      rewrite Z add0n /task_arrivals_between /arrivals_between big_nat1.

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

1 subgoal (ID 513)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
        task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
        task_arrivals_between arr_seq tsk (task_offset tsk)
          (task_offset tsk).+1
  Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
  ============================
  size [seq j <- arrivals_at arr_seq (task_offset tsk) | job_task j == tsk] =
  1

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

      specialize (task_arrivals_at_size 0) ⇒ AT_SIZE.

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

1 subgoal (ID 516)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
        task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
        task_arrivals_between arr_seq tsk (task_offset tsk)
          (task_offset tsk).+1
  Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
  AT_SIZE : let l := task_offset tsk + 0 * task_period tsk in
            size (task_arrivals_at arr_seq tsk l) = 1
  ============================
  size [seq j <- arrivals_at arr_seq (task_offset tsk) | job_task j == tsk] =
  1

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

      now rewrite mul0n addn0 in AT_SIZE.

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

No more subgoals.

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

    Qed.

We show that for any number [n], the number of jobs released by task [tsk] up to [task_offset tsk + n * task_period tsk] is equal to [n + 1].
    Lemma task_arrivals_up_to_size:
      ∀ n,
        let l := (task_offset tsk + n × task_period tsk) in
        let r := (task_offset tsk + n.+1 × task_period tsk) in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1.

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

1 subgoal (ID 132)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  ============================
  forall n : nat,
  let l := task_offset tsk + n * task_period tsk in
  let r := task_offset tsk + n.+1 * task_period tsk in
  size (task_arrivals_up_to arr_seq tsk l) = n + 1

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

    Proof.
      induction n.

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

2 subgoals (ID 137)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  ============================
  let l := task_offset tsk + 0 * task_period tsk in
  let r := task_offset tsk + 1 * task_period tsk in
  size (task_arrivals_up_to arr_seq tsk l) = 0 + 1

subgoal 2 (ID 140) is:
 let l := task_offset tsk + n.+1 * task_period tsk in
 let r := task_offset tsk + n.+2 * task_period tsk in
 size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1

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

      intros l r; rewrite /l mul0n add0n addn0.

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

2 subgoals (ID 158)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  l := task_offset tsk + 0 * task_period tsk : nat
  r := task_offset tsk + 1 * task_period tsk : nat
  ============================
  size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1

subgoal 2 (ID 140) is:
 let l := task_offset tsk + n.+1 * task_period tsk in
 let r := task_offset tsk + n.+2 * task_period tsk in
 size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1

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

      now apply size_task_arrivals_up_to_offset.

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

1 subgoal (ID 140)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  ============================
  let l := task_offset tsk + n.+1 * task_period tsk in
  let r := task_offset tsk + n.+2 * task_period tsk in
  size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1

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

      intros l r.

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

1 subgoal (ID 160)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  ============================
  size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1

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

      specialize (task_arrivals_cat arr_seq tsk (task_offset tsk + n × task_period tsk)
                                    (task_offset tsk + n.+1 × task_period tsk)) ⇒ CAT.

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

1 subgoal (ID 174)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_offset tsk + n * task_period tsk <=
        task_offset tsk + n.+1 * task_period tsk ->
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1

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

      feed_n 1 CAT; first by ssrlia.

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

1 subgoal (ID 180)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1

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

      rewrite CAT size_cat IHn.

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

1 subgoal (ID 973)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  n + 1 +
  size
    (task_arrivals_between arr_seq tsk
       (task_offset tsk + n * task_period tsk).+1
       (task_offset tsk + n.+1 * task_period tsk).+1) = 
  n.+1 + 1

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

      specialize (task_arrivals_between_cat arr_seq tsk (task_offset tsk + n × task_period tsk).+1
                 (task_offset tsk + n.+1 × task_period tsk) (task_offset tsk + n.+1 × task_period tsk).+1) ⇒ S_CAT.

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

1 subgoal (ID 991)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  S_CAT : task_offset tsk + n * task_period tsk <
          task_offset tsk + n.+1 * task_period tsk ->
          task_offset tsk + n.+1 * task_period tsk <=
          (task_offset tsk + n.+1 * task_period tsk).+1 ->
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk).+1 =
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk) ++
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n.+1 * task_period tsk)
            (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  n + 1 +
  size
    (task_arrivals_between arr_seq tsk
       (task_offset tsk + n * task_period tsk).+1
       (task_offset tsk + n.+1 * task_period tsk).+1) = 
  n.+1 + 1

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

      feed_n 2 S_CAT; try by ssrlia.

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

2 subgoals (ID 992)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  S_CAT : task_offset tsk + n * task_period tsk <
          task_offset tsk + n.+1 * task_period tsk ->
          task_offset tsk + n.+1 * task_period tsk <=
          (task_offset tsk + n.+1 * task_period tsk).+1 ->
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk).+1 =
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk) ++
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n.+1 * task_period tsk)
            (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  task_offset tsk + n * task_period tsk <
  task_offset tsk + n.+1 * task_period tsk

subgoal 2 (ID 1003) is:
 n + 1 +
 size
   (task_arrivals_between arr_seq tsk
      (task_offset tsk + n * task_period tsk).+1
      (task_offset tsk + n.+1 * task_period tsk).+1) = 
 n.+1 + 1

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

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

1 subgoal (ID 992)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  S_CAT : task_offset tsk + n * task_period tsk <
          task_offset tsk + n.+1 * task_period tsk ->
          task_offset tsk + n.+1 * task_period tsk <=
          (task_offset tsk + n.+1 * task_period tsk).+1 ->
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk).+1 =
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk) ++
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n.+1 * task_period tsk)
            (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  task_offset tsk + n * task_period tsk <
  task_offset tsk + n.+1 * task_period tsk

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

rewrite ltn_add2l ltn_mul2r.

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

1 subgoal (ID 4928)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  S_CAT : task_offset tsk + n * task_period tsk <
          task_offset tsk + n.+1 * task_period tsk ->
          task_offset tsk + n.+1 * task_period tsk <=
          (task_offset tsk + n.+1 * task_period tsk).+1 ->
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk).+1 =
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk) ++
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n.+1 * task_period tsk)
            (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  (0 < task_period tsk) && (n < n.+1)

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

        now apply /andP; split ⇒ //.

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

1 subgoal

subgoal 1 (ID 1003) is:
 n + 1 +
 size
   (task_arrivals_between arr_seq tsk
      (task_offset tsk + n * task_period tsk).+1
      (task_offset tsk + n.+1 * task_period tsk).+1) = 
 n.+1 + 1

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

      }

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

1 subgoal (ID 1003)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  S_CAT : task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk).+1 =
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk) ++
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n.+1 * task_period tsk)
            (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  n + 1 +
  size
    (task_arrivals_between arr_seq tsk
       (task_offset tsk + n * task_period tsk).+1
       (task_offset tsk + n.+1 * task_period tsk).+1) = 
  n.+1 + 1

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

      rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.

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

1 subgoal (ID 4980)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  S_CAT : task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk).+1 =
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk) ++
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n.+1 * task_period tsk)
            (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  n + 1 +
  (size
     [seq j <- \cat_((task_offset tsk + n * task_period tsk).+1<=t<
               task_offset tsk + n.+1 * task_period tsk)
               arrivals_at arr_seq t
        | job_task j == tsk] +
   size
     [seq j <- arrivals_at arr_seq (task_offset tsk + n.+1 * task_period tsk)
        | job_task j == tsk]) = n.+1 + 1

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

      rewrite size_task_arrivals_between_eq0 task_arrivals_at_size ⇒ //.

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

1 subgoal (ID 4986)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n : nat
  IHn : let l := task_offset tsk + n * task_period tsk in
        let r := task_offset tsk + n.+1 * task_period tsk in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1
  l := task_offset tsk + n.+1 * task_period tsk : nat
  r := task_offset tsk + n.+2 * task_period tsk : nat
  CAT : task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n.+1 * task_period tsk) =
        task_arrivals_up_to arr_seq tsk
          (task_offset tsk + n * task_period tsk) ++
        task_arrivals_between arr_seq tsk
          (task_offset tsk + n * task_period tsk).+1
          (task_offset tsk + n.+1 * task_period tsk).+1
  S_CAT : task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk).+1 =
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n * task_period tsk).+1
            (task_offset tsk + n.+1 * task_period tsk) ++
          task_arrivals_between arr_seq tsk
            (task_offset tsk + n.+1 * task_period tsk)
            (task_offset tsk + n.+1 * task_period tsk).+1
  ============================
  n + 1 + (0 + 1) = n.+1 + 1

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

      now ssrlia.

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

No more subgoals.

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

    Qed.

We show that the number of jobs released by task [tsk] at any instant [t] and [t + n * task_period tsk] is the same for any number [n].
    Lemma eq_size_of_task_arrivals_seperated_by_period:
      ∀ n t,
        t ≥ task_offset tsk →
        size (task_arrivals_at arr_seq tsk t) =
        size (task_arrivals_at arr_seq tsk (t + n × task_period tsk)).

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

1 subgoal (ID 148)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  ============================
  forall n t : nat,
  task_offset tsk <= t ->
  size (task_arrivals_at arr_seq tsk t) =
  size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

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

    Proof.
      intros × T_G.

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

1 subgoal (ID 151)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n, t : nat
  T_G : task_offset tsk <= t
  ============================
  size (task_arrivals_at arr_seq tsk t) =
  size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

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

      destruct (exists_or_not_add_mul_cases (task_offset tsk) (task_period tsk) t) as [[n1 JB_ARR] | JB_NOT_ARR].

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

2 subgoals (ID 166)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n, t : nat
  T_G : task_offset tsk <= t
  n1 : nat
  JB_ARR : t = task_offset tsk + n1 * task_period tsk
  ============================
  size (task_arrivals_at arr_seq tsk t) =
  size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

subgoal 2 (ID 167) is:
 size (task_arrivals_at arr_seq tsk t) =
 size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

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

      + have EXISTS_N : ∃ nn, t + n × task_period tsk = task_offset tsk + nn × task_period tsk.

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

3 subgoals (ID 177)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n, t : nat
  T_G : task_offset tsk <= t
  n1 : nat
  JB_ARR : t = task_offset tsk + n1 * task_period tsk
  ============================
  exists nn : nat,
    t + n * task_period tsk = task_offset tsk + nn * task_period tsk

subgoal 2 (ID 179) is:
 size (task_arrivals_at arr_seq tsk t) =
 size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 3 (ID 167) is:
 size (task_arrivals_at arr_seq tsk t) =
 size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

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

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

1 subgoal (ID 177)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n, t : nat
  T_G : task_offset tsk <= t
  n1 : nat
  JB_ARR : t = task_offset tsk + n1 * task_period tsk
  ============================
  exists nn : nat,
    t + n * task_period tsk = task_offset tsk + nn * task_period tsk

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

∃ (n1 + n).

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

1 subgoal (ID 181)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n, t : nat
  T_G : task_offset tsk <= t
  n1 : nat
  JB_ARR : t = task_offset tsk + n1 * task_period tsk
  ============================
  t + n * task_period tsk = task_offset tsk + (n1 + n) * task_period tsk

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

          now rewrite JB_ARR; ssrlia.

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

2 subgoals

subgoal 1 (ID 179) is:
 size (task_arrivals_at arr_seq tsk t) =
 size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 2 (ID 167) is:
 size (task_arrivals_at arr_seq tsk t) =
 size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

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

        }

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

2 subgoals (ID 179)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n, t : nat
  T_G : task_offset tsk <= t
  n1 : nat
  JB_ARR : t = task_offset tsk + n1 * task_period tsk
  EXISTS_N : exists nn : nat,
               t + n * task_period tsk =
               task_offset tsk + nn * task_period tsk
  ============================
  size (task_arrivals_at arr_seq tsk t) =
  size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

subgoal 2 (ID 167) is:
 size (task_arrivals_at arr_seq tsk t) =
 size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

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

        move : EXISTS_N ⇒ [nn JB_ARR'].

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

2 subgoals (ID 365)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n, t : nat
  T_G : task_offset tsk <= t
  n1 : nat
  JB_ARR : t = task_offset tsk + n1 * task_period tsk
  nn : nat
  JB_ARR' : t + n * task_period tsk = task_offset tsk + nn * task_period tsk
  ============================
  size (task_arrivals_at arr_seq tsk t) =
  size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

subgoal 2 (ID 167) is:
 size (task_arrivals_at arr_seq tsk t) =
 size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

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

        now rewrite JB_ARR' JB_ARR !task_arrivals_at_size ⇒ //.

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

1 subgoal (ID 167)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n, t : nat
  T_G : task_offset tsk <= t
  JB_NOT_ARR : forall n : nat, t <> task_offset tsk + n * task_period tsk
  ============================
  size (task_arrivals_at arr_seq tsk t) =
  size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

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

      + have FORALL_N : ∀ nn, t + n × task_period tsk ≠ task_offset tsk + nn × task_period tsk by apply mul_add_neq.

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

1 subgoal (ID 389)
  
  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
  tsk : Task
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  H_infinite_jobs : infinite_jobs arr_seq
  n, t : nat
  T_G : task_offset tsk <= t
  JB_NOT_ARR : forall n : nat, t <> task_offset tsk + n * task_period tsk
  FORALL_N : forall nn : nat,
             t + n * task_period tsk <>
             task_offset tsk + nn * task_period tsk
  ============================
  size (task_arrivals_at arr_seq tsk t) =
  size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))

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

        now rewrite !task_arrivals_size_at_non_arrival.

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

No more subgoals.

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

    Qed.

  End TaskArrivalsInCaseOfInfiniteJobs.

End TaskArrivalsSize.