diff --git a/analysis/definitions/hyperperiod.v b/analysis/definitions/hyperperiod.v
index 700f9f7904c0a21ece7f963896c99d1eff51b2e9..0d7bad8f6a86a52ed19fe582e946445b1d04abd5 100644
--- a/analysis/definitions/hyperperiod.v
+++ b/analysis/definitions/hyperperiod.v
@@ -5,29 +5,75 @@ From mathcomp Require Import div.
 (** In this file we define the notion of a hyperperiod for periodic tasks. *)
 Section Hyperperiod.
 
-  (** Consider periodic tasks. *)
+  (** Consider any type of periodic tasks ... *)
   Context {Task : TaskType} `{PeriodicModel Task}.
 
-  (** Consider any task set [ts]... *)
+  (** ... and any task set [ts]. *)
   Variable ts : TaskSet Task.
 
-  (** ... and any task [tsk] that belongs to this task set. *)
-  Variable tsk : Task.
-  Hypothesis H_tsk_in_ts : tsk \in ts.
-
   (** The hyperperiod of a task set is defined as the least common multiple
-   (LCM) of the periods of all tasks in the task set. **)
+      (LCM) of the periods of all tasks in the task set. **)
   Definition hyperperiod : duration := lcml (map task_period ts).        
 
-  (** Consequently, a task set's hyperperiod is an integral multiple
-   of each task's period in the task set. **)
-  Lemma hyperperiod_int_mult_of_any_task : 
-    exists k, hyperperiod = k * task_period tsk.
-  Proof.
-    apply lcm_seq_is_mult_of_all_ints.
-    apply map_f.
-    by apply H_tsk_in_ts.
-  Qed.
-
 End Hyperperiod.
 
+(** In this section we provide basic definitions concerning the hyperperiod
+    of all tasks in a task set. *)
+Section HyperperiodDefinitions.
+
+  (** Consider any type of periodic tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskOffset Task}.
+  Context `{PeriodicModel Task}.
+
+  (** ... and any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+
+  (** Consider any task set [ts] ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... and any arrival sequence [arr_seq]. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** Let [O_max] denote the maximum offset of all tasks in [ts] ... *)
+  Let O_max := max_task_offset ts.
+
+  (** ... and let [HP] denote the hyperperiod of all tasks in [ts]. *)
+  Let HP := hyperperiod ts.
+
+  (** We define a hyperperiod index based on an instant [t]
+      which lies in it. *)
+  (** Note that we consider the first hyperperiod to start at time [O_max], 
+      i.e., shifted by the maximum offset (and not at time zero as can also 
+      be found sometimes in the literature) *)
+  Definition hyperperiod_index (t : instant) :=
+    (t - O_max) %/ HP.
+
+  (** Given an instant [t], we define the starting instant of the hyperperiod 
+   that contains [t]. *)
+  Definition starting_instant_of_hyperperiod (t : instant) :=
+    hyperperiod_index t * HP + O_max.
+
+  (** Given a job [j], we define the starting instant of the hyperperiod
+   in which [j] arrives. *)
+  Definition starting_instant_of_corresponding_hyperperiod (j : Job) :=
+    starting_instant_of_hyperperiod (job_arrival j).
+
+  (** We define the sequence of jobs of a task [tsk] that arrive in a hyperperiod
+      given the starting instant [h] of the hyperperiod. *)
+  Definition jobs_in_hyperperiod (h : instant) (tsk : Task) :=
+    task_arrivals_between arr_seq tsk h (h + HP).
+
+  (** We define the index of a job [j] of task [tsk] in a hyperperiod starting at [h]. *)
+  Definition job_index_in_hyperperiod (j : Job) (h : instant) (tsk : Task) :=
+    index j (jobs_in_hyperperiod h tsk).
+
+  (** Given a job [j] of task [tsk] and the hyperperiod starting at [h], we define a 
+      [corresponding_job_in_hyperperiod] which is the job that arrives in given hyperperiod 
+      and has the same [job_index] as [j]. *)
+  Definition corresponding_job_in_hyperperiod (j : Job) (h : instant) (tsk : Task) :=
+    nth j (jobs_in_hyperperiod h tsk) (job_index_in_hyperperiod j (starting_instant_of_corresponding_hyperperiod j) tsk).
+
+End HyperperiodDefinitions.
diff --git a/analysis/definitions/infinite_jobs.v b/analysis/definitions/infinite_jobs.v
new file mode 100644
index 0000000000000000000000000000000000000000..07ab48a52ca2453563c71bb657149d605783e2fe
--- /dev/null
+++ b/analysis/definitions/infinite_jobs.v
@@ -0,0 +1,28 @@
+Require Export prosa.model.task.arrivals.
+
+(** In this section we define the notion of an infinite release 
+    of jobs by a task. *)
+Section InfiniteJobs.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+
+  (** Consider any arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** We say that a task [tsk] releases an infinite number of jobs 
+      if for every integer [n] there exists a job [j] of task [tsk]
+      such that [job_index] of [j] is equal to [n]. *)
+  Definition infinite_jobs :=
+    forall tsk n,
+    exists j,
+      arrives_in arr_seq j /\
+      job_task j = tsk /\
+      job_index arr_seq j = n.
+  
+End InfiniteJobs.
diff --git a/analysis/definitions/job_response_time.v b/analysis/definitions/job_response_time.v
new file mode 100644
index 0000000000000000000000000000000000000000..78375007ff4e61b9d43a3caf425995c5c0b72f80
--- /dev/null
+++ b/analysis/definitions/job_response_time.v
@@ -0,0 +1,24 @@
+Require Export prosa.behavior.all.
+
+(** In this section we define what it means for the response time 
+    of a job to exceed some given duration. *)
+Section JobResponseTimeExceeds.
+
+  (** Consider any kind of jobs ... *)
+  Context {Job : JobType}.
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+
+  (** ... and any kind of processor state. *)
+  Context `{PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  (** We say that a job [j] has a response time exceeding a number [x] 
+      if [j] is pending [x] units of time after its arrival. *)
+  Definition job_response_time_exceeds (j : Job) (x : duration) :=
+    ~~ completed_by sched j ((job_arrival j) + x).
+
+End JobResponseTimeExceeds.
diff --git a/analysis/facts/hyperperiod.v b/analysis/facts/hyperperiod.v
new file mode 100644
index 0000000000000000000000000000000000000000..6ba6b68d5bcb03271b0248532bae3e3b994ccb17
--- /dev/null
+++ b/analysis/facts/hyperperiod.v
@@ -0,0 +1,246 @@
+Require Export prosa.analysis.definitions.hyperperiod.
+Require Export prosa.analysis.facts.periodic.task_arrivals_size.
+Require Export prosa.util.div_mod.
+
+(** In this file we prove some simple properties of hyperperiods of periodic tasks. *)
+Section Hyperperiod.
+
+  (** Consider any type of periodic tasks, ... *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** ... any task set [ts], ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... and any task [tsk] that belongs to this task set. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts: tsk \in ts.
+
+  (** A task set's hyperperiod is an integral multiple
+      of each task's period in the task set. **)
+  Lemma hyperperiod_int_mult_of_any_task: 
+    exists (k : nat),
+      hyperperiod ts = k * task_period tsk.
+  Proof.
+    apply lcm_seq_is_mult_of_all_ints.
+    apply map_f.
+    now apply H_tsk_in_ts.
+  Qed.
+
+End Hyperperiod.
+
+(** In this section we show a property of hyperperiod in context 
+   of task sets with valid periods. *)
+Section ValidPeriodsImplyPositiveHP.
+
+  (** Consider any type of periodic tasks ... *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** ... and any task set [ts] ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... such that all tasks in [ts] have valid periods. *)
+  Hypothesis H_valid_periods: valid_periods ts.
+
+  (** We show that the hyperperiod of task set [ts] 
+   is positive. *)
+  Lemma valid_periods_imply_pos_hp:
+    hyperperiod ts > 0.
+  Proof.
+    apply all_pos_implies_lcml_pos.
+    move => b /mapP [x IN EQ]; subst b.
+    now apply H_valid_periods.
+  Qed.
+  
+End ValidPeriodsImplyPositiveHP.
+
+(** In this section we prove some lemmas about the hyperperiod
+    in context of the periodic model. *)
+Section PeriodicLemmas.
+
+  (** Consider any type of tasks, ... *)
+  Context {Task : TaskType}.
+  Context `{TaskOffset Task}.
+  Context `{PeriodicModel Task}.
+
+  (** ... any type of jobs, ... *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  
+  (** ... and a consistent arrival sequence with non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
+  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
+  
+  (** Consider a task set [ts] such that all tasks in
+      [ts] have valid periods. *)
+  Variable ts : TaskSet Task.
+  Hypothesis H_valid_periods: valid_periods ts.
+
+  (** Let [tsk] be any periodic task in [ts] with a valid offset and period. *)
+  Variable tsk : Task.
+  Hypothesis H_task_in_ts: tsk \in ts.
+  Hypothesis H_valid_offset: valid_offset arr_seq tsk.
+  Hypothesis H_valid_period: valid_period tsk.
+  Hypothesis H_periodic_task: respects_periodic_task_model arr_seq tsk.
+
+  (** Assume we have an infinite sequence of jobs in the arrival sequence. *)
+  Hypothesis H_infinite_jobs: infinite_jobs arr_seq.
+  
+  (** Let [O_max] denote the maximum task offset in [ts] and let
+   [HP] denote the hyperperiod of all tasks in [ts]. *)
+  Let O_max := max_task_offset ts.
+  Let HP := hyperperiod ts.
+
+  (** We show that the job corresponding to any job [j1] in any other
+      hyperperiod is of the same task as [j1]. *)
+  Lemma corresponding_jobs_have_same_task:
+    forall j1 j2,
+      job_task (corresponding_job_in_hyperperiod ts arr_seq j1
+               (starting_instant_of_corresponding_hyperperiod ts j2) (job_task j1)) = job_task j1.
+  Proof.
+    intros *.
+    set ARRIVALS := (task_arrivals_between arr_seq (job_task j1) (starting_instant_of_hyperperiod ts (job_arrival j2))
+          (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)).
+    set IND := (job_index_in_hyperperiod ts arr_seq j1 (starting_instant_of_hyperperiod ts (job_arrival j1)) (job_task j1)).
+    have SIZE_G : size ARRIVALS <= IND -> job_task (nth j1 ARRIVALS IND) = job_task j1 by intro SG; rewrite nth_default.
+    case: (boolP (size ARRIVALS == IND)) => [/eqP EQ|NEQ]; first by apply SIZE_G; ssrlia.
+    move : NEQ; rewrite neq_ltn; move => /orP [LT | G]; first by apply SIZE_G; ssrlia.
+    set jb := nth j1 ARRIVALS IND.
+    have JOB_IN : jb \in ARRIVALS by apply mem_nth.
+    rewrite /ARRIVALS /task_arrivals_between mem_filter in JOB_IN.
+    now move : JOB_IN => /andP [/eqP TSK JB_IN].
+  Qed.    
+
+  (** We show that if a job [j] lies in the hyperperiod starting
+   at instant [t] then [j] arrives in the interval <<[t, t + HP)>>. *)
+  Lemma all_jobs_arrive_within_hyperperiod:
+    forall j t,
+      j \in jobs_in_hyperperiod ts arr_seq t tsk->
+      t <= job_arrival j < t + HP.
+  Proof.
+    intros * JB_IN_HP.
+    rewrite mem_filter in JB_IN_HP.
+    move : JB_IN_HP => /andP [/eqP TSK JB_IN]; apply mem_bigcat_nat_exists in JB_IN.
+    destruct JB_IN as [i [JB_IN INEQ]]; apply H_consistent_arrivals in JB_IN.
+    now rewrite JB_IN.
+  Qed.
+  
+  (** We show that the number of jobs in a hyperperiod starting at [n1 * HP + O_max] 
+   is the same as the number of jobs in a hyperperiod starting at [n2 * HP + O_max] given 
+   that [n1] is less than or equal to [n2]. *)
+  Lemma eq_size_hyp_lt:
+    forall n1 n2,
+      n1 <= n2 ->
+      size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
+      size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk).
+  Proof.
+    intros * N1_LT.
+    specialize (add_mul_diff n1 n2 HP O_max) => AD; feed_n 1 AD => //.
+    rewrite AD.
+    destruct (hyperperiod_int_mult_of_any_task ts tsk H_task_in_ts) as [k HYP]; rewrite !/HP.
+    rewrite [in X in _ = size (_ (n1 * HP + O_max + _ * X) tsk)]HYP.
+    rewrite mulnA /HP /jobs_in_hyperperiod !size_of_task_arrivals_between.
+    erewrite big_sum_eq_in_eq_sized_intervals => //; intros g G_LT.
+    have OFF_G : task_offset tsk <= O_max by apply max_offset_g.
+    have FG : forall v b n, v + b + n = v + n + b by intros *; ssrlia.
+    erewrite eq_size_of_task_arrivals_seperated_by_period => //; last by ssrlia.
+    now rewrite FG.
+  Qed.
+
+  (** We generalize the above lemma by lifting the condition on 
+   [n1] and [n2]. *)
+  Lemma eq_size_of_arrivals_in_hyperperiod:
+    forall n1 n2,
+      size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
+      size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk).
+  Proof.
+    intros *.
+    case : (boolP (n1 == n2)) => [/eqP EQ | NEQ]; first by rewrite EQ.
+    move : NEQ; rewrite neq_ltn; move => /orP [LT | LT].
+    + now apply eq_size_hyp_lt => //; ssrlia.
+    + move : (eq_size_hyp_lt n2 n1) => EQ_S.
+      now feed_n 1 EQ_S => //; ssrlia.
+  Qed.
+
+  (** Consider any two jobs [j1] and [j2] that stem from the arrival sequence
+   [arr_seq] such that [j1] is of task [tsk]. *)
+  Variable j1 : Job.
+  Variable j2 : Job.
+  Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
+  Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
+  Hypothesis H_j1_task: job_task j1 = tsk.
+
+  (** Assume that both [j1] and [j2] arrive after [O_max]. *)
+  Hypothesis H_j1_arr_after_O_max: O_max <= job_arrival j1.
+  Hypothesis H_j2_arr_after_O_max: O_max <= job_arrival j2.
+
+  (** We show that any job [j] that arrives in task arrivals in the same 
+      hyperperiod as [j2] also arrives in task arrivals up to [job_arrival j2 + HP]. *)
+  Lemma job_in_hp_arrives_in_task_arrivals_up_to:
+    forall j,
+      j \in jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk ->
+      j \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
+  Proof.
+    intros j J_IN.
+    rewrite /task_arrivals_up_to.
+    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk).
+    move : (J_IN) => J_ARR; apply all_jobs_arrive_within_hyperperiod in J_IN.
+    rewrite /jobs_in_hp /jobs_in_hyperperiod /task_arrivals_up_to /task_arrivals_between mem_filter in J_ARR.
+    move : J_ARR =>  /andP [/eqP TSK' NTH_IN].
+    apply job_in_task_arrivals_between => //; first by apply in_arrivals_implies_arrived in NTH_IN.
+    apply mem_bigcat_nat_exists in NTH_IN.
+    move : NTH_IN => [i [NJ_IN INEQ]]; apply H_consistent_arrivals in NJ_IN; rewrite -NJ_IN in INEQ.
+    apply /andP; split => //.
+    rewrite ltnS.
+    apply leq_trans with (n := (job_arrival j2 - O_max) %/ HP * HP + O_max + HP); first by ssrlia.
+    rewrite leq_add2r.
+    have O_M : (job_arrival j2 - O_max) %/ HP * HP <= job_arrival j2 - O_max by apply leq_trunc_div.
+    have ARR_G : job_arrival j2 >= O_max by auto.
+    now ssrlia.
+  Qed.
+
+  (** We show that job [j1] arrives in its own hyperperiod. *)
+  Lemma job_in_own_hp:
+    j1 \in jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk.
+  Proof.
+    apply job_in_task_arrivals_between => //.
+    apply /andP; split.
+    + rewrite addnC -leq_subRL => //.
+      now apply leq_trunc_div.
+    + specialize (div_floor_add_g (job_arrival j1 - O_max) HP) => AB.
+      feed_n 1 AB; first by apply valid_periods_imply_pos_hp => //.
+      apply ltn_subLR in AB.
+      now rewrite -/(HP); ssrlia.
+  Qed.
+
+  (** We show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod
+   arrives in task arrivals up to [job_arrival j2 + HP]. *)
+  Lemma corr_job_in_task_arrivals_up_to:
+    corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk \in
+      task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
+  Proof.
+    rewrite /corresponding_job_in_hyperperiod /starting_instant_of_corresponding_hyperperiod.
+    rewrite /job_index_in_hyperperiod /starting_instant_of_hyperperiod /hyperperiod_index.
+    set ind := (index j1 (jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk)).
+    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk).
+    set nj := nth j1 jobs_in_hp ind.
+    apply job_in_hp_arrives_in_task_arrivals_up_to => //.
+    rewrite mem_nth /jobs_in_hp => //.
+    specialize (eq_size_of_arrivals_in_hyperperiod ((job_arrival j2 - O_max) %/ HP) ((job_arrival j1 - O_max) %/ HP)) => EQ.
+    rewrite EQ /ind index_mem.
+    now apply job_in_own_hp.
+  Qed.    
+
+  (** Finally, we show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod 
+   arrives in the arrival sequence [arr_seq]. *)
+  Lemma corresponding_job_arrives:
+      arrives_in arr_seq (corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk).
+  Proof.
+    move : (corr_job_in_task_arrivals_up_to) => ARR_G.
+    rewrite /task_arrivals_up_to /task_arrivals_between mem_filter in ARR_G.
+    move : ARR_G =>  /andP [/eqP TSK' NTH_IN].
+    now apply in_arrivals_implies_arrived in NTH_IN.
+  Qed.
+
+End PeriodicLemmas.
diff --git a/analysis/facts/model/offset.v b/analysis/facts/model/offset.v
index c1c1f68408f93fc5ab544dacad38871e010c539b..c19f246cb91b341a16677a90b61e709f773b9bb9 100644
--- a/analysis/facts/model/offset.v
+++ b/analysis/facts/model/offset.v
@@ -1,7 +1,7 @@
 Require Export prosa.model.task.offset.
 Require Export prosa.analysis.facts.job_index.
 
-(** In this module, we'll prove a property of task offsets. *)
+(** In this module, we prove some properties of task offsets. *)
 Section OffsetLemmas.
   
   (** Consider any type of tasks with an offset ... *)
@@ -13,12 +13,13 @@ Section OffsetLemmas.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
 
-  (** Consider any arrival sequence with consistent and non-duplicate arrivals, ... *)
+  (** Consider any arrival sequence with consistent and non-duplicate arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
   Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
-  (** ... and any job [j] of any task [tsk] with a valid offset. *)
+  (** ... and any job [j] (that stems from the arrival sequence) of any 
+      task [tsk] with a valid offset. *)
   Variable tsk : Task.
   Variable j : Job.
   Hypothesis H_job_of_task: job_task j = tsk.
@@ -43,5 +44,20 @@ Section OffsetLemmas.
       now apply/eqP; rewrite eqn_leq; apply/andP; split;
         [ssrlia | apply H_valid_offset].
   Qed.
-  
+
+  (** Consider any task set [ts]. *)
+  Variable ts : TaskSet Task.
+
+  (** If task [tsk] is in [ts], then its offset
+   is less than or equal to the maximum offset of all tasks 
+   in [ts]. *)
+  Lemma max_offset_g:
+    tsk \in ts ->
+    task_offset tsk <= max_task_offset ts.
+  Proof.
+    intros TSK_IN.
+    apply in_max0_le.
+    now apply map_f.
+  Qed.
+
 End OffsetLemmas.
diff --git a/analysis/facts/model/task_arrivals.v b/analysis/facts/model/task_arrivals.v
index a198f0220c423349e57c8a5e0076ad90a7553878..73cbb564aff2a9bb2f86538dd8311db48c238f8a 100644
--- a/analysis/facts/model/task_arrivals.v
+++ b/analysis/facts/model/task_arrivals.v
@@ -13,7 +13,7 @@ Section TaskArrivals.
   
   (** Consider any job arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
+  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
   
   (** We show that the number of arrivals of task can be split into disjoint intervals. *) 
   Lemma num_arrivals_of_task_cat:
@@ -133,19 +133,30 @@ Section TaskArrivals.
     now apply arrived_between_implies_in_arrivals.
   Qed.
 
+  (** Any job [j] in [task_arrivals_between arr_seq tsk t1 t2] arrives 
+      in the arrival sequence [arr_seq]. *)
+  Lemma arrives_in_task_arrivals_implies_arrived:
+    forall t1 t2 j,
+      j \in (task_arrivals_between arr_seq tsk t1 t2) ->
+      arrives_in arr_seq j.
+  Proof.
+    intros * JB_IN.
+    move : JB_IN; rewrite mem_filter; move => /andP [/eqP TSK JB_IN].
+    now apply in_arrivals_implies_arrived in JB_IN.
+  Qed.
+    
   (** An arrival sequence with non-duplicate arrivals implies that the 
       task arrivals also contain non-duplicate arrivals. *)
   Lemma uniq_task_arrivals:
-    forall j,
-      arrives_in arr_seq j ->
+    forall t,
       arrival_sequence_uniq arr_seq ->
-      uniq (task_arrivals_up_to arr_seq (job_task j) (job_arrival j)).
+      uniq (task_arrivals_up_to arr_seq tsk t).
   Proof.
-    intros j ARR UNQ_ARR.
+    intros * UNQ_SEQ.
     apply filter_uniq.
     now apply arrivals_uniq.
   Qed.
-
+  
   (** A job cannot arrive before it's arrival time. *) 
   Lemma job_notin_task_arrivals_before:
     forall j t, 
@@ -180,5 +191,58 @@ Section TaskArrivals.
     - rewrite /task_arrivals_up_to_job_arrival TSK1 TSK2.
       now rewrite -task_arrivals_cat; try by ssrlia.
   Qed.
-  
+
+  (** For any job [j2] with [job_index] equal to [n], the nth job 
+   in the sequence [task_arrivals_up_to arr_seq tsk t] is [j2], given that
+   [t] is not less than [job_arrival j2]. *)
+  (** Note that [j_def] is used as a default job for the access function and
+   has nothing to do with the lemma. *)
+  Lemma nth_job_of_task_arrivals:
+    forall n j_def j t,
+      arrives_in arr_seq j ->
+      job_task j = tsk ->
+      job_index arr_seq j = n ->
+      t >= job_arrival j ->
+      nth j_def (task_arrivals_up_to arr_seq tsk t) n = j.
+  Proof.
+    intros * ARR TSK IND T_G.
+    rewrite -IND.
+    have EQ_IND : index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t).
+    { have CAT : exists xs, task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t.
+      { rewrite /task_arrivals_up_to_job_arrival TSK.
+        exists (task_arrivals_between arr_seq tsk ((job_arrival j).+1) t.+1).
+        now rewrite -task_arrivals_cat.
+      }
+      move : CAT => [xs ARR_CAT].
+      now rewrite -ARR_CAT index_cat ifT; last by apply arrives_in_task_arrivals_up_to.
+    }
+    rewrite /job_index EQ_IND nth_index => //.
+    rewrite mem_filter; apply /andP.
+    split; first by apply /eqP.
+    now apply job_in_arrivals_between => //.
+  Qed.
+
+  (** We show that task arrivals in the interval <<[t1, t2)>> 
+   is the same as concatenation of task arrivals at each instant in <<[t1, t2)>>. *)
+  Lemma task_arrivals_between_is_cat_of_task_arrivals_at:
+    forall t1 t2,
+      task_arrivals_between arr_seq tsk t1 t2 = \cat_(t1 <= t < t2) task_arrivals_at arr_seq tsk t.
+  Proof.
+    intros *.
+    rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.
+    now apply cat_filter_eq_filter_cat.
+  Qed.
+
+  (** The number of jobs of a task [tsk] in the interval <<[t1, t2)>> is the same 
+   as sum of the number of jobs of the task [tsk] at each instant in <<[t1, t2)>>. *)
+  Lemma size_of_task_arrivals_between:
+    forall t1 t2,
+      size (task_arrivals_between arr_seq tsk t1 t2)
+      = \sum_(t1 <= t < t2) size (task_arrivals_at arr_seq tsk t). 
+  Proof.
+    intros *.
+    rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.
+    now rewrite size_big_nat cat_filter_eq_filter_cat.
+  Qed.
+    
 End TaskArrivals.
diff --git a/analysis/facts/periodic/arrival_times.v b/analysis/facts/periodic/arrival_times.v
index 32246de75c2f6e01707fccea7573a30d5955e1eb..164cf83f3145f77ef36b0b7f0200fa4a0c3a38f8 100644
--- a/analysis/facts/periodic/arrival_times.v
+++ b/analysis/facts/periodic/arrival_times.v
@@ -49,5 +49,47 @@ Section PeriodicArrivalTimes.
       rewrite ARRIVAL IHn; ssrlia.
     }
   Qed.
+
+  (** We show that for every job [j] of task [tsk] there exists a number 
+   [n] such that [j] arrives at the instant [task_offset tsk + n * task_period tsk]. *)
+  Lemma job_arrival_times:
+    forall j,
+      arrives_in arr_seq j ->
+      job_task j = tsk ->
+      exists n, job_arrival j = task_offset tsk + n * task_period tsk.
+  Proof.
+    intros * ARR TSK.
+    exists (job_index arr_seq j).
+    specialize (periodic_arrival_times (job_index arr_seq j) j) => J_ARR.
+    now feed_n 3 J_ARR => //.
+  Qed.
+
+  (** If a job [j] of task [tsk] arrives at [task_offset tsk + n * task_period tsk] 
+   then the [job_index] of [j] is equal to [n]. *)
+  Lemma job_arr_index:
+    forall 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.
+  Proof.
+    have F : task_period tsk > 0 by auto.
+    induction n.
+    + intros * ARR_J TSK ARR.
+      destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] => //. 
+      now apply periodic_arrival_times in SUCC => //; ssrlia.
+    + intros * ARR_J TSK ARR.
+      specialize (H_task_respects_periodic_model j); feed_n 3 H_task_respects_periodic_model => //.
+      { rewrite lt0n; apply /eqP; intro EQ.
+        apply first_job_arrival with (tsk0 := tsk) in EQ => //.
+        now rewrite EQ in ARR; ssrlia.
+      }
+      move : H_task_respects_periodic_model => [j' [ARR' [IND' [TSK' [ARRIVAL']]]]].
+      specialize (IHn j'); feed_n 3 IHn => //; first by rewrite ARR in ARRIVAL'; ssrlia.
+      rewrite IHn in IND'.
+      destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by ssrlia.
+      apply first_job_arrival with (tsk0 := tsk) in Z => //.
+      now rewrite Z in ARR; ssrlia.
+  Qed.
   
 End PeriodicArrivalTimes.
diff --git a/analysis/facts/periodic/task_arrivals_size.v b/analysis/facts/periodic/task_arrivals_size.v
new file mode 100644
index 0000000000000000000000000000000000000000..d6d454f45ffad0f0c686b462e408593c8c253826
--- /dev/null
+++ b/analysis/facts/periodic/task_arrivals_size.v
@@ -0,0 +1,202 @@
+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:
+    forall t,
+      (forall n, t <> task_offset tsk + n * task_period tsk) ->
+      task_arrivals_at arr_seq tsk t = [::].
+  Proof.
+    intros * T.
+    have EMPT_OR_EXISTS : forall xs, xs = [::] \/ exists a, a \in xs.
+    { intros *.
+      induction xs; first by left.
+      right; exists a.
+      now apply mem_head.
+    }
+    destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] => //.
+    rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN => /andP [/eqP TSK A_ARR].
+    move : (A_ARR) => A_IN; apply H_consistent_arrivals in A_IN.
+    rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.
+    apply in_arrseq_implies_arrives in A_ARR.
+    have EXISTS_N : exists n, job_arrival a = task_offset tsk + n * task_period tsk by
+          apply job_arrival_times with (arr_seq0 := arr_seq) => //.
+    move : EXISTS_N => [n A_ARRIVAL].
+    now move : (T n) => T1.
+  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: 
+    forall t,
+      size (task_arrivals_at arr_seq tsk t) = 0 \/
+      size (task_arrivals_at arr_seq tsk t) = 1.
+  Proof.
+    intro t.
+    case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) => [LT|GT|EQ]; try by auto.
+    destruct (size (task_arrivals_at arr_seq tsk t)); now left.
+    specialize (exists_two Job (task_arrivals_at arr_seq tsk t)) => EXISTS_TWO.
+    destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].
+    rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
+    move: A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
+    move: (ARRA); move: (ARRB); rewrite /arrivals_at => A_IN B_IN.
+    apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
+    have SPO : respects_sporadic_task_model arr_seq tsk; try by auto with basic_facts.
+    have EQ_ARR_A : (job_arrival a = t) by apply H_consistent_arrivals.
+    have EQ_ARR_B : (job_arrival b = t) by apply H_consistent_arrivals.
+    specialize (SPO a b); feed_n 6 SPO => //; try by ssrlia.
+    rewrite EQ_ARR_A EQ_ARR_B in SPO.
+    rewrite /task_min_inter_arrival_time /periodic_as_sporadic in SPO.
+    have POS : task_period tsk > 0 by auto.
+    now ssrlia.
+  Qed.
+
+  (** We show that the size of task arrivals (strictly) between two consecutive arrival
+      times is zero. *)
+  Lemma size_task_arrivals_between_eq0:
+    forall 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.
+  Proof.
+    intros n l r; rewrite /l /r.
+    rewrite size_of_task_arrivals_between big_nat_eq0 => //; intros t INEQ.
+    rewrite task_arrivals_size_at_non_arrival => //; intros n1 EQ.
+    rewrite EQ in INEQ.
+    move : INEQ => /andP [INEQ1 INEQ2].
+    rewrite ltn_add2l ltn_mul2r in INEQ1; rewrite ltn_add2l ltn_mul2r in INEQ2.
+    move : INEQ1 INEQ2 => /andP [A B] /andP [C D].
+    now ssrlia.
+  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:
+      forall n,
+      exists 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.
+    Proof.
+      intros *.
+      destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].
+      exists j; repeat split => //.
+      now apply periodic_arrival_times with (arr_seq0 := arr_seq) => //.
+    Qed.
+    
+    (** We show that the size of task arrivals at any arrival time is equal to one. *)
+    Lemma task_arrivals_at_size:
+      forall n,
+        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.
+      move : (jobs_exists_later n) => [j' [ARR [TSK [ARRIVAL IND]]]].
+      apply only_j_in_task_arrivals_at_j with (tsk0 := tsk) in ARR => //; last by
+          auto with basic_facts.
+      rewrite /task_arrivals_at_job_arrival TSK in ARR.
+      now rewrite -ARRIVAL ARR.
+    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.
+    Proof.
+      rewrite /task_arrivals_up_to.
+      specialize (task_arrivals_between_cat arr_seq tsk 0 (task_offset tsk) (task_offset tsk).+1) => CAT.
+      feed_n 2 CAT => //; rewrite CAT size_cat.
+      have Z : 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.
+        rewrite task_arrivals_size_at_non_arrival => //; intros n EQ.
+        now ssrlia.
+      }               
+      rewrite Z add0n /task_arrivals_between /arrivals_between big_nat1.
+      specialize (task_arrivals_at_size 0) => AT_SIZE.
+      now rewrite mul0n addn0 in AT_SIZE.
+    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:
+      forall 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.
+    Proof.
+      induction n.
+      intros l r; rewrite /l mul0n add0n addn0.
+      now apply size_task_arrivals_up_to_offset.
+      intros l r.
+      specialize (task_arrivals_cat arr_seq tsk (task_offset tsk + n * task_period tsk)
+                                    (task_offset tsk + n.+1 * task_period tsk)) => CAT.
+      feed_n 1 CAT; first by ssrlia.
+      rewrite CAT size_cat IHn.
+      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.
+      feed_n 2 S_CAT; try by ssrlia.
+      { rewrite ltn_add2l ltn_mul2r.
+        now apply /andP; split => //.
+      }
+      rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.
+      rewrite size_task_arrivals_between_eq0 task_arrivals_at_size => //.
+      now ssrlia.
+    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:
+      forall 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)).
+    Proof.
+      intros * T_G.
+      destruct (exists_or_not_add_mul_cases (task_offset tsk) (task_period tsk) t) as [[n1 JB_ARR] | JB_NOT_ARR].
+      + have EXISTS_N : exists nn, t + n * task_period tsk = task_offset tsk + nn * task_period tsk.
+        { exists (n1 + n).
+          now rewrite JB_ARR; ssrlia.
+        }
+        move : EXISTS_N => [nn JB_ARR'].
+        now rewrite JB_ARR' JB_ARR !task_arrivals_at_size => //.
+      + have FORALL_N : forall nn, t + n * task_period tsk <> task_offset tsk + nn * task_period tsk by apply mul_add_neq.
+        now rewrite !task_arrivals_size_at_non_arrival.
+    Qed.
+    
+  End TaskArrivalsInCaseOfInfiniteJobs.
+  
+End TaskArrivalsSize.
diff --git a/analysis/facts/shifted_job_costs.v b/analysis/facts/shifted_job_costs.v
new file mode 100644
index 0000000000000000000000000000000000000000..5cd9b2c620a6009f9502fdf9b0f6cace5c047538
--- /dev/null
+++ b/analysis/facts/shifted_job_costs.v
@@ -0,0 +1,89 @@
+Require Export prosa.analysis.facts.periodic.arrival_times.
+Require Export prosa.analysis.facts.periodic.task_arrivals_size.
+Require Export prosa.model.task.concept.
+Require Export prosa.analysis.facts.hyperperiod.
+
+(** In this file we define a new function for job costs 
+    in an observation interval and prove its validity. *)
+Section ValidJobCostsShifted.
+
+  (** Consider any type of periodic tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskOffset Task}.
+  Context `{PeriodicModel Task}.
+  Context `{TaskCost Task}.
+
+  (** ... and any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobDeadline Job}.
+  
+  (** Consider a consistent arrival sequence with non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
+  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
+
+  (** Furthermore, assume that arrivals have valid job costs. *) 
+  Hypothesis H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq.
+  
+  (** Consider a periodic task set [ts] such that all tasks in
+      [ts] have valid periods and offsets. *)
+  Variable ts : TaskSet Task.
+  Hypothesis H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts.
+  Hypothesis H_valid_periods_in_taskset: valid_periods ts. 
+  Hypothesis H_valid_offsets_in_taskset: valid_offsets arr_seq ts.
+  
+  (** Consider a job [j] that stems from the arrival sequence. *)
+  Variable j : Job.
+  Hypothesis H_j_from_arrival_sequence: arrives_in arr_seq j.
+
+  (** Let [O_max] denote the maximum task offset of all tasks in [ts] ... *)
+  Let O_max := max_task_offset ts.
+  (** ... and let [HP] denote the hyperperiod of all tasks in [ts]. *)
+  Let HP := hyperperiod ts.
+
+  (** We now define a new function for job costs in the observation interval. *)
+
+  (** Given that job [j] arrives after [O_max], the cost of a job [j'] 
+   that arrives in the interval <<[O_max + HP, O_max + 2HP)>> is defined to 
+   be the same as the job cost of its corresponding job in [j]'s hyperperiod. *)
+  Definition job_costs_shifted (j' : Job) :=
+    if (job_arrival j >= O_max) && (O_max + HP <= job_arrival j' < O_max + 2 * HP) then
+      job_cost (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j'))
+    else job_cost j'.
+  
+  (** Assume that we have an infinite sequence of jobs. *)
+  Hypothesis H_infinite_jobs: infinite_jobs arr_seq. 
+
+  (** Assume all jobs in the arrival sequence [arr_seq] belong to some task 
+   in [ts]. *)
+  Hypothesis H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts.
+
+  (** We assign the job costs as defined by the [job_costs_shifted] function. *)
+  Instance job_costs_in_oi : JobCost Job :=
+    job_costs_shifted.
+
+  (** We show that the [job_costs_shifted] function is valid. *)
+  Lemma job_costs_shifted_valid: arrivals_have_valid_job_costs arr_seq.
+  Proof.
+    rewrite /arrivals_have_valid_job_costs /valid_job_cost.
+    intros j' ARR.
+    unfold job_cost; rewrite /job_costs_in_oi /job_costs_shifted.
+    destruct (leqP O_max (job_arrival j)) as [A | B].
+    destruct (leqP (O_max + HP) (job_arrival j')) as [NEQ | NEQ].
+    destruct (leqP (O_max + 2 * HP) (job_arrival j')) as [LT | LT].
+    all : try by apply H_arrivals_have_valid_job_costs => //.
+    simpl.
+    specialize (corresponding_jobs_have_same_task arr_seq ts j' j) => TSK.
+    rewrite -[in X in _ <= task_cost X]TSK.
+    have IN : job_task j' \in ts by apply H_jobs_from_taskset.
+    apply H_arrivals_have_valid_job_costs, corresponding_job_arrives => //.
+    + now apply H_valid_offsets_in_taskset.
+    + now apply H_valid_periods_in_taskset.  
+    + now apply H_periodic_taskset.
+    + now ssrlia.
+  Qed.
+
+End ValidJobCostsShifted.
diff --git a/analysis/facts/sporadic.v b/analysis/facts/sporadic.v
index 5074335c6804dfa1fb25f43adfbc2505a347be1d..ea07ae03be39e3f179fd3f248af24c73d1f76900 100644
--- a/analysis/facts/sporadic.v
+++ b/analysis/facts/sporadic.v
@@ -89,7 +89,7 @@ Section DifferentJobsImplyDifferentArrivalTimes.
   Hypothesis H_j1_task: job_task j1 = tsk.
   Hypothesis H_j2_task: job_task j2 = tsk.
 
-  (** We observe that unequal jobs cannot have equal arrival times. *)
+  (** We observe that distinct jobs cannot have equal arrival times. *)
   Lemma uneq_job_uneq_arr:
       j1 <> j2 ->
       job_arrival j1 <> job_arrival j2.
@@ -99,7 +99,22 @@ Section DifferentJobsImplyDifferentArrivalTimes.
     move /neqP: UNEQ; rewrite neq_ltn => /orP [LT|LT].
     all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia.
   Qed.
-  
+
+  (** We prove a stronger version of the above lemma by showing 
+   that jobs [j1] and [j2] are equal if and only if they arrive at the
+   same time. *)
+  Lemma same_jobs_iff_same_arr:
+    j1 = j2 <->
+    job_arrival j1 = job_arrival j2.
+  Proof.
+    split; first by apply congr1.
+    intro EQ_ARR.
+    case: (boolP (j1 == j2)) => [/eqP EQ | /eqP NEQ]; first by auto.
+    rewrite -> diff_jobs_iff_diff_indices in NEQ => //; auto; last by rewrite H_j1_task.
+    move /neqP: NEQ; rewrite neq_ltn => /orP [LT|LT].
+    all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia.
+  Qed.
+    
 End DifferentJobsImplyDifferentArrivalTimes.
 
 (** In this section we prove a few properties regarding task arrivals
@@ -157,8 +172,8 @@ Section SporadicArrivals.
     apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
     have EQ_ARR_A : (job_arrival a = job_arrival j) by apply H_consistent_arrivals.
     have EQ_ARR_B : (job_arrival b = job_arrival j) by apply H_consistent_arrivals.
-    apply (uneq_job_uneq_arr arr_seq) with (tsk0 := job_task a) in NEQ => //; try by rewrite TSKA.
-    now ssrlia.
+    apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j) in NEQ => //.
+    now rewrite EQ_ARR_A EQ_ARR_B in NEQ.
   Qed.
 
   (** We show that no jobs of the task [tsk] other than [j1] arrive at
@@ -182,6 +197,20 @@ Section SporadicArrivals.
       exists j1.
       now repeat split => //; try rewrite H_j1_task.
   Qed.
+
+  (** We show that no jobs of the task [tsk] other than [j1] arrive at
+      the same time as [j1], and thus the task arrivals at [job arrival j1]
+      consists only of job [j1]. *) 
+  Lemma only_j_at_job_arrival_j:
+    forall t,
+      job_arrival j1 = t ->
+      task_arrivals_at arr_seq tsk t = [::j1]. 
+  Proof.
+    intros t ARR.
+    rewrite -ARR.
+    specialize (only_j_in_task_arrivals_at_j) => J_AT.
+    now rewrite /task_arrivals_at_job_arrival H_j1_task in J_AT.
+  Qed.
   
   (** We show that a job [j1] is the first job that arrives 
       in task arrivals at [job_arrival j1] by showing that the 
diff --git a/model/task/offset.v b/model/task/offset.v
index bf695c0f0afce81ea87fad4e931515bdb0cbd2a7..31c5291fbaf0e3a5cb8dda74f58f3b2110de076b 100644
--- a/model/task/offset.v
+++ b/model/task/offset.v
@@ -51,5 +51,21 @@ Section ValidTaskOffset.
   
 End ValidTaskOffset.
 
+(** In this section we define the notion of a maximum task offset. *)
+Section MaxTaskOffset.
 
+  (** Consider any type of tasks with offsets, ... *)
+  Context {Task : TaskType}.
+  Context `{TaskOffset Task}.
+  
+  (** ... and any task set. *)
+  Variable ts : TaskSet Task.
+
+  (** We define the sequence of task offsets of all tasks in [ts], ... *)
+  Definition task_offsets := map task_offset ts.
+
+  (** ... and the maximum among all the task offsets. *)
+  Definition max_task_offset := max0 task_offsets.
+    
+End MaxTaskOffset.
 
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index d73451a5a12d83300291ac7203bf7699f70e1a32..4e3df729c7a88eedbc616172f468b22cf377cea3 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -49,6 +49,7 @@ bursty
 TODO
 mathcomp
 hyperperiod
+hyperperiods
 pointwise
 notational
 multiset
diff --git a/util/bigcat.v b/util/bigcat.v
index 9843c6a34ab1697613d83bda6149b14b2cc5d5d7..1444b8dccc27fcbc1f5b0de561d19998ebb9b00e 100644
--- a/util/bigcat.v
+++ b/util/bigcat.v
@@ -1,5 +1,6 @@
 Require Export prosa.util.tactics prosa.util.notation.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.util.tactics prosa.util.ssrlia.
 
 (** In this section, we introduce useful lemmas about the concatenation operation performed
     over an arbitrary range of sequences. *)
@@ -34,7 +35,7 @@ Section BigCatLemmas.
 
     (** Conversely, we prove that any element belonging to a concatenation of sequences 
         must come from one of the sequences. *)
-    Lemma mem_bigcat_nat_exists :
+    Lemma mem_bigcat_nat_exists:
       forall x m n,
         x \in \cat_(m <= i < n) (f i) ->
         exists i,
@@ -84,7 +85,7 @@ Section BigCatLemmas.
       forall x i1 i2, x \in f i1 -> x \in f i2 -> i1 = i2.
     
     (** We prove that the concatenation will yield a sequence with unique elements. *)
-    Lemma bigcat_nat_uniq :
+    Lemma bigcat_nat_uniq:
       forall n1 n2,
         uniq (\cat_(n1 <= i < n2) (f i)).
     Proof.
@@ -146,4 +147,43 @@ Section BigCatLemmas.
 
   End BigCatDistinctElements.
 
+  (**  We show that filtering a concatenated sequence by any predicate [P] 
+   is the same as concatenating the elements of the sequence that satisfy [P]. *) 
+  Lemma cat_filter_eq_filter_cat:
+    forall {X : Type} (F : nat -> seq X) (P : X -> bool) (t1 t2 : nat),
+      [seq x <- \cat_(t1<=t<t2) F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x].
+  Proof.
+    intros.
+    specialize (leq_total t1 t2) => /orP [T1_LT | T2_LT].
+    + have EX: exists Δ, t2 = t1 + Δ by exists (t2 - t1); ssrlia.
+      move: EX => [Δ EQ]; subst t2.
+      induction Δ.
+      { now rewrite addn0 !big_geq => //. }
+      { rewrite addnS !big_nat_recr => //=; try by rewrite leq_addr.
+        rewrite filter_cat IHΔ => //.
+        now ssrlia.
+      }
+    + now rewrite !big_geq => //.
+  Qed.
+
+  (** We show that the size of a concatenated sequence is the same as 
+   summation of sizes of each element of the sequence. *)
+  Lemma size_big_nat: 
+    forall {X : Type} (F : nat -> seq X) (t1 t2 : nat),
+      \sum_(t1 <= t < t2) size (F t) =
+      size (\cat_(t1 <= t < t2) F t).
+  Proof.
+    intros.
+    specialize (leq_total t1 t2) => /orP [T1_LT | T2_LT].
+    + have EX: exists Δ, t2 = t1 + Δ by exists (t2 - t1); ssrlia.
+      move: EX => [Δ EQ]; subst t2.
+      induction Δ.
+      { now rewrite addn0 !big_geq => //. }
+      { rewrite addnS !big_nat_recr => //=; try by rewrite leq_addr.
+        rewrite size_cat IHΔ => //.
+        now ssrlia.
+      }         
+    + now rewrite !big_geq => //.
+  Qed.      
+      
 End BigCatLemmas.
diff --git a/util/div_mod.v b/util/div_mod.v
index af257be9d60fff599dd6de9e3ceae099f0c2be0f..60347602daaafacc99e791a2c0d911ba4bbfd4c4 100644
--- a/util/div_mod.v
+++ b/util/div_mod.v
@@ -18,3 +18,16 @@ Proof.
   - rewrite modn_small;try ssrlia.
 Qed.
 
+(** We show that for any two integers [a] and [c], 
+    [a] is less than [a %/ c * c + c] given that [c] is positive. *)
+Lemma div_floor_add_g:
+  forall a c,
+    c > 0 ->
+    a < a %/ c * c + c.
+Proof.
+  intros * POS.
+  specialize (divn_eq a c) => DIV.
+  rewrite [in X in X < _]DIV.
+  rewrite ltn_add2l.
+  now apply ltn_pmod.
+Qed.    
diff --git a/util/lcmseq.v b/util/lcmseq.v
index 4407c40dbc0da43c4346f8ea9d97ae21ae58002c..628d0ffd9b85cae9a20937e91bb918234338a4b4 100644
--- a/util/lcmseq.v
+++ b/util/lcmseq.v
@@ -1,11 +1,12 @@
 From mathcomp Require Export ssreflect seq div ssrbool ssrnat eqtype ssrfun.
+Require Export prosa.util.tactics.
 
 (** A function to calculate the least common multiple 
     of all integers in a sequence [xs], denoted by [lcml xs]  **)
 Definition lcml (xs : seq nat) : nat := foldr lcmn 1 xs.
 
 (** Any integer [a] that is contained in the sequence [xs] divides [lcml xs]. **)
-Lemma int_divides_lcm_in_seq : 
+Lemma int_divides_lcm_in_seq: 
   forall (a : nat) (xs : seq nat), a %| lcml (a :: xs).
 Proof.
   intros.
@@ -19,7 +20,7 @@ Proof.
 Qed.
 
 (** Also, [lcml xs1] divides [lcml xs2] if [xs2] contains one extra element as compared to [xs1]. *)
-Lemma lcm_seq_divides_lcm_super : 
+Lemma lcm_seq_divides_lcm_super: 
   forall (x : nat) (xs : seq nat), 
   lcml xs %| lcml (x :: xs).
 Proof.
@@ -31,7 +32,7 @@ Proof.
 Qed.
 
 (** All integers in a sequence [xs] divide [lcml xs]. *)
-Lemma lcm_seq_is_mult_of_all_ints : 
+Lemma lcm_seq_is_mult_of_all_ints: 
   forall (sq : seq nat) (a : nat), a \in sq -> exists k, lcml sq = k * a. 
 Proof.
   intros xs x IN.
@@ -46,3 +47,22 @@ Proof.
     rewrite -mulnA -EQ divnK /lcml //.
     by apply lcm_seq_divides_lcm_super.
 Qed.
+
+(** The LCM of all elements in a sequence with only positive elements is positive. *)
+Lemma all_pos_implies_lcml_pos:
+  forall (xs : seq nat),
+    (forall b, b \in xs -> b > 0) ->
+    lcml xs > 0.
+Proof.
+  intros * POS.
+  induction xs; first by easy.
+  rewrite /lcml -cat1s => //.
+  simpl; rewrite lcmn_gt0.
+  apply /andP; split => //.
+  + apply POS; rewrite in_cons; apply /orP; left.
+    now apply /eqP.
+  + feed_n 1 IHxs.
+    - intros b B_IN.
+      now apply POS; rewrite in_cons; apply /orP; right => //.
+    - now rewrite /lcml in IHxs.
+Qed.
diff --git a/util/nat.v b/util/nat.v
index b267c5cb82316d4f473832baa87b326bf667c389..524f50ba1194c31e35f603d858b6d261962471be 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -4,13 +4,13 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop d
 (* Additional lemmas about natural numbers. *)
 Section NatLemmas.
 
-  Lemma subh1 :
+  Lemma subh1:
     forall m n p,
       m >= n ->
       m - n + p = m + p - n.
   Proof. by ins; ssrlia. Qed.
 
-  Lemma subh2 :
+  Lemma subh2:
     forall m1 m2 n1 n2,
       m1 >= m2 ->
       n1 >= n2 ->
@@ -48,7 +48,7 @@ Section NatLemmas.
     forall a b c,
       a >= c ->
       b >=c ->
-      a + (b - c ) = a - c + b.
+      a + (b - c) = a - c + b.
   Proof.
     intros* AgeC BgeC.
     induction b;induction c;intros;try ssrlia.
@@ -74,10 +74,62 @@ Section NatLemmas.
     by apply leq_addr.
   Qed.
 
+  (** For any numbers [a], [b], and [m], either there exists a number [n] 
+   such that [m = a + n * b] or [m <> a + n * b] for any [n]. *)
+  Lemma exists_or_not_add_mul_cases:
+    forall a b m,
+      (exists n, m = a + n * b) \/
+      (forall n, m <> a + n * b).
+  Proof.
+    move=> a b m.
+    case: (leqP a  m) => LE.
+    { case: (boolP(b %| (m - a))) => DIV.
+      { left; exists ((m - a) %/ b).
+        now rewrite divnK //   subnKC //. }
+      { right. move=> n EQ.
+        move: DIV => /negP DIV; apply DIV.
+        rewrite EQ.
+        rewrite -addnBAC // subnn add0n.
+        apply dvdn_mull.
+        now apply dvdnn. }}
+    { right; move=> n EQ.
+      move: LE; rewrite EQ.
+      now rewrite -ltn_subRL subnn //. }
+  Qed.
+
+  (** The expression [n2 * a + b] can be written as [n1 * a + b + (n2 - n1) * a]
+      for any integer [n1] such that [n1 <= n2]. *)
+  Lemma add_mul_diff:
+    forall n1 n2 a b,
+      n1 <= n2 ->
+      n2 * a + b = n1 * a + b + (n2 - n1) * a.
+  Proof.
+    intros * LT.
+    rewrite mulnBl.
+    rewrite addnBA; first by ssrlia.
+    destruct a; first by ssrlia.
+    now rewrite leq_pmul2r.
+  Qed.
+
+  (** Given constants [a, b, c, z] such that [b <= a] and there is no constant [m] 
+      such that [a = b + m * c], it holds that there is no constant [n] such that 
+      [a + z * c = b + n * c]. *)
+  Lemma mul_add_neq: 
+    forall a b c z,
+      b <= a ->
+      (forall m, a <> b + m * c) -> 
+      forall n, a + z * c <> b + n * c.
+  Proof.
+    intros * LTE NEQ n EQ.
+    specialize (NEQ (n - z)).
+    rewrite mulnBl in NEQ.
+    now ssrlia.
+  Qed.
+  
 End NatLemmas.
 
 Section Interval.
-
+  
   (* Trivially, points before the start of an interval, or past the end of an
      interval, are not included in the interval. *)
   Lemma point_not_in_interval:
diff --git a/util/sum.v b/util/sum.v
index 32f72e1e9185c45753afc138710257c34d3f352a..89d1d2139217afcddfdfe9fada5f62c5ca726ba3 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -198,7 +198,7 @@ Section ExtraLemmas.
 
   (* We show that the fact that the sum is smaller than the range 
      of the summation implies the existence of a zero element. *)
-  Lemma sum_le_summation_range :
+  Lemma sum_le_summation_range:
     forall f t Δ,
       \sum_(t <= x < t + Δ) f x < Δ ->
       exists x, t <= x < t + Δ /\ f x = 0.
@@ -217,6 +217,27 @@ Section ExtraLemmas.
         by rewrite ltnS ltnW.
     }
   Qed.
+
+  (** If a function [F] gives same values at [t1 + g] and [t2 + g] for all [g] strictly
+      less than an integer [d] and for any [t1] and [t2], then summation of [F] over
+      the intervals <<[t1, t1 + d)>> and <<[t2, t2 + d)>> is equal. *)
+  Lemma big_sum_eq_in_eq_sized_intervals:
+    forall t1 t2 d (F1 F2 : nat -> nat),
+      (forall g, g < d -> F1 (t1 + g) = F2 (t2 + g)) -> 
+      \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t.
+  Proof.
+    intros * P.
+    induction d.
+    now rewrite !addn0 !big_geq => //.
+    feed_n 1 IHd.
+    { intros g G_LT.
+      now specialize (P g); feed_n 1 P; ssrlia.
+    }
+    rewrite !addnS !big_nat_recr => //; try by ssrlia.
+    rewrite IHd.
+    specialize (P d); feed_n 1 P. ssrlia.
+    now rewrite P.
+  Qed.
   
 End ExtraLemmas.