diff --git a/analysis/facts/periodic/arrival_separation.v b/analysis/facts/periodic/arrival_separation.v
index 89ed08c0e9aadc15a0ea93840996f019440d6a7c..d4cee86db38416ae419d61c5624bc01e5963b0a1 100644
--- a/analysis/facts/periodic/arrival_separation.v
+++ b/analysis/facts/periodic/arrival_separation.v
@@ -1,5 +1,5 @@
Require Export prosa.analysis.facts.periodic.sporadic.
-Require Export prosa.analysis.facts.sporadic.
+Require Export prosa.analysis.facts.sporadic.arrival_times.
(** In this section we show that the separation between job
arrivals of a periodic task is some multiple of their
diff --git a/analysis/facts/periodic/task_arrivals_size.v b/analysis/facts/periodic/task_arrivals_size.v
index 587383df7a0d54ebed0f67e4fd0121b47eceb606..a92967c94fb474fccf6336b725f38bd3ff2c926a 100644
--- a/analysis/facts/periodic/task_arrivals_size.v
+++ b/analysis/facts/periodic/task_arrivals_size.v
@@ -1,5 +1,6 @@
Require Export prosa.analysis.facts.periodic.arrival_times.
Require Export prosa.analysis.definitions.infinite_jobs.
+Require Export prosa.analysis.facts.sporadic.arrival_sequence.
(** In this file we prove some properties concerning the size
of task arrivals in context of the periodic model. *)
diff --git a/analysis/facts/sporadic.v b/analysis/facts/sporadic/arrival_sequence.v
similarity index 59%
rename from analysis/facts/sporadic.v
rename to analysis/facts/sporadic/arrival_sequence.v
index 453661ca45cfc296b33afca662e4eb3da83c8e3a..79fba642539bd22b9eb10273975f5eba5334570e 100644
--- a/analysis/facts/sporadic.v
+++ b/analysis/facts/sporadic/arrival_sequence.v
@@ -1,116 +1,9 @@
-Require Export prosa.model.task.arrival.sporadic.
-Require Export prosa.analysis.facts.job_index.
+Require Export analysis.facts.sporadic.arrival_times.
-(** * The Sporadic Model *)
+(** * Job Arrival Sequence in the Sporadic Model *)
-(** In this section we prove a few basic properties involving
- job indices in context of the sporadic model. *)
-Section SporadicModelIndexLemmas.
-
- (** Consider sporadic tasks ... *)
- Context {Task : TaskType} `{SporadicModel Task}.
-
- (** ... and any type of jobs associated with these tasks. *)
- Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
-
- (** Consider any unique arrival sequence with consistent arrivals, ... *)
- Variable arr_seq : arrival_sequence Job.
- Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
- Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
-
- (** ... and any sporadic task [tsk] that is to be analyzed. *)
- Variable tsk : Task.
- Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
- Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
-
- (** Consider any two jobs from the arrival sequence that stem
- from task [tsk]. *)
- Variable j1 : Job.
- Variable j2 : Job.
- Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
- Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
- Hypothesis H_j1_task: job_task j1 = tsk.
- Hypothesis H_j2_task: job_task j2 = tsk.
-
- (** We first show that for any two jobs [j1] and [j2], [j2] arrives after [j1]
- provided [job_index] of [j2] strictly exceeds the [job_index] of [j1]. *)
- Lemma lower_index_implies_earlier_arrival:
- job_index arr_seq j1 < job_index arr_seq j2 ->
- job_arrival j1 < job_arrival j2.
- Proof.
- move=> LT_IND.
- move: (H_sporadic_model j1 j2) => SPORADIC; feed_n 6 SPORADIC => //.
- - rewrite -> diff_jobs_iff_diff_indices => //; eauto; first by lia.
- by subst.
- - apply (index_lte_implies_arrival_lte arr_seq); try eauto.
- by subst.
- - have POS_IA : task_min_inter_arrival_time tsk > 0 by auto.
- by lia.
- Qed.
-
-End SporadicModelIndexLemmas.
-
-(** ** Different jobs have different arrival times. *)
-Section DifferentJobsImplyDifferentArrivalTimes.
-
- (** Consider sporadic tasks ... *)
- Context {Task : TaskType} `{SporadicModel Task}.
-
- (** ... and any type of jobs associated with these tasks. *)
- Context {Job : JobType}.
- Context `{JobTask Job Task}.
- Context `{JobArrival Job}.
-
- (** Consider any unique arrival sequence with consistent arrivals, ... *)
- Variable arr_seq : arrival_sequence Job.
- Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
- Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
-
- (** ... and any sporadic task [tsk] that is to be analyzed. *)
- Variable tsk : Task.
- Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
- Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
-
- (** Consider any two jobs from the arrival sequence that stem
- from task [tsk]. *)
- Variable j1 : Job.
- Variable j2 : Job.
- Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
- Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
- Hypothesis H_j1_task: job_task j1 = tsk.
- Hypothesis H_j2_task: job_task j2 = tsk.
-
- (** We observe that distinct jobs cannot have equal arrival times. *)
- Lemma uneq_job_uneq_arr:
- j1 <> j2 ->
- job_arrival j1 <> job_arrival j2.
- Proof.
- intros UNEQ EQ_ARR.
- rewrite -> diff_jobs_iff_diff_indices in UNEQ => //; eauto; last by rewrite H_j1_task.
- move /neqP: UNEQ; rewrite neq_ltn => /orP [LT|LT].
- all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) ||
- now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
- 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 => //; eauto; last by rewrite H_j1_task.
- move /neqP: NEQ; rewrite neq_ltn => /orP [LT|LT].
- all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) || now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
- Qed.
-
-End DifferentJobsImplyDifferentArrivalTimes.
-
-(** In this section we prove a few properties regarding task arrivals
- in context of the sporadic task model. *)
+(** In this file, we prove basic facts about a task's arrival sequence
+ in the sporadic task model. *)
Section SporadicArrivals.
(** Consider sporadic tasks ... *)
diff --git a/analysis/facts/sporadic/arrival_times.v b/analysis/facts/sporadic/arrival_times.v
new file mode 100644
index 0000000000000000000000000000000000000000..493738f3268e80275a18df6b42925e1d059a0861
--- /dev/null
+++ b/analysis/facts/sporadic/arrival_times.v
@@ -0,0 +1,111 @@
+Require Export prosa.model.task.arrival.sporadic.
+Require Export prosa.analysis.facts.job_index.
+
+(** * Job Arrival Times in the Sporadic Model *)
+
+(** In this file, we prove a few basic facts about the arrival times
+ of jobs in the sporadic task model. *)
+Section SporadicModelIndexLemmas.
+
+ (** Consider sporadic tasks ... *)
+ Context {Task : TaskType} `{SporadicModel Task}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
+
+ (** Consider any unique arrival sequence with consistent arrivals, ... *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
+ Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
+
+ (** ... and any sporadic task [tsk] that is to be analyzed. *)
+ Variable tsk : Task.
+ Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
+ Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
+
+ (** Consider any two jobs from the arrival sequence that stem
+ from task [tsk]. *)
+ Variable j1 : Job.
+ Variable j2 : Job.
+ Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
+ Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
+ Hypothesis H_j1_task: job_task j1 = tsk.
+ Hypothesis H_j2_task: job_task j2 = tsk.
+
+ (** We first show that for any two jobs [j1] and [j2], [j2] arrives after [j1]
+ provided [job_index] of [j2] strictly exceeds the [job_index] of [j1]. *)
+ Lemma lower_index_implies_earlier_arrival:
+ job_index arr_seq j1 < job_index arr_seq j2 ->
+ job_arrival j1 < job_arrival j2.
+ Proof.
+ move=> LT_IND.
+ move: (H_sporadic_model j1 j2) => SPORADIC; feed_n 6 SPORADIC => //.
+ - rewrite -> diff_jobs_iff_diff_indices => //; eauto; first by lia.
+ by subst.
+ - apply (index_lte_implies_arrival_lte arr_seq); try eauto.
+ by subst.
+ - have POS_IA : task_min_inter_arrival_time tsk > 0 by auto.
+ by lia.
+ Qed.
+
+End SporadicModelIndexLemmas.
+
+(** ** Different jobs have different arrival times. *)
+Section DifferentJobsImplyDifferentArrivalTimes.
+
+ (** Consider sporadic tasks ... *)
+ Context {Task : TaskType} `{SporadicModel Task}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobArrival Job}.
+
+ (** Consider any unique arrival sequence with consistent arrivals, ... *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
+ Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
+
+ (** ... and any sporadic task [tsk] that is to be analyzed. *)
+ Variable tsk : Task.
+ Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
+ Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
+
+ (** Consider any two jobs from the arrival sequence that stem
+ from task [tsk]. *)
+ Variable j1 : Job.
+ Variable j2 : Job.
+ Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
+ Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
+ Hypothesis H_j1_task: job_task j1 = tsk.
+ Hypothesis H_j2_task: job_task j2 = tsk.
+
+ (** We observe that distinct jobs cannot have equal arrival times. *)
+ Lemma uneq_job_uneq_arr:
+ j1 <> j2 ->
+ job_arrival j1 <> job_arrival j2.
+ Proof.
+ intros UNEQ EQ_ARR.
+ rewrite -> diff_jobs_iff_diff_indices in UNEQ => //; eauto; last by rewrite H_j1_task.
+ move /neqP: UNEQ; rewrite neq_ltn => /orP [LT|LT].
+ all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) ||
+ now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
+ 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 => //; eauto; last by rewrite H_j1_task.
+ move /neqP: NEQ; rewrite neq_ltn => /orP [LT|LT].
+ all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) || now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
+ Qed.
+
+End DifferentJobsImplyDifferentArrivalTimes.
+