diff --git a/model/schedule/uni/limited/abstract_RTA/abstract_rta.v b/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
index 621e1306b6ea4c498b76bbe4107a7fd79565c1b8..d6bd459e1dcc2f6adcb6d35515d599dd2da1d56f 100644
--- a/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
+++ b/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
@@ -15,8 +15,8 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
 Module AbstractRTA. 
 
-  Import Job Epsilon UniprocessorSchedule Service ResponseTime 
-         AbstractRTADefinitions AbstractRTALockInService AbstractRTAReduction. 
+  Import Job UniprocessorSchedule Service ResponseTime  AbstractRTADefinitions
+         AbstractRTALockInService AbstractRTAReduction. 
 
   (* In this section we prove that the maximum among the solutions of the response-time bound 
      recurrence is a response time bound for tsk. Note that in this section we do not rely on 
diff --git a/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v b/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
index 45783244467b94347af01b6f807157e515e1ac15..4c6fe76a1e2246bcbf3caa788adfd54b4b93f778 100644
--- a/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
+++ b/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
@@ -23,7 +23,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     and sequential jobs. *)
 Module AbstractSeqRTA. 
 
-  Import Job Epsilon ArrivalCurves TaskArrival ScheduleOfTask UniprocessorSchedule Workload
+  Import Job ArrivalCurves TaskArrival ScheduleOfTask UniprocessorSchedule Workload
          Service ResponseTime MaxArrivalsWorkloadBound 
          AbstractRTADefinitions AbstractRTALockInService AbstractRTAReduction AbstractRTA. 
 
diff --git a/model/schedule/uni/limited/abstract_RTA/definitions.v b/model/schedule/uni/limited/abstract_RTA/definitions.v
index 2bf00e6268df35a3e66c86e8823b700545af75a5..09e0cc709a41a71ace35b2255044ea82a3c09c6a 100644
--- a/model/schedule/uni/limited/abstract_RTA/definitions.v
+++ b/model/schedule/uni/limited/abstract_RTA/definitions.v
@@ -9,7 +9,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
 Module AbstractRTADefinitions. 
 
-  Import Job Epsilon UniprocessorSchedule.
+  Import Job UniprocessorSchedule.
 
   (* In this section, we introduce all the abstract notions required by the analysis. *)
   Section Definitions.
diff --git a/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v b/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
index 9ce65a850a25940338453aabb993279dc2a1beed..dded10d6cc49632d0292cdc467646f2388ae4b99 100644
--- a/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
+++ b/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
@@ -10,7 +10,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
    
 Module AbstractRTAReduction. 
 
-  Import Epsilon UniprocessorSchedule.
+  Import UniprocessorSchedule.
 
   (* The response-time analysis we are presenting in this series of documents is based on searching 
      over all possible values of A, the relative arrival time of the job respective to the beginning 
diff --git a/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v b/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
index cd31ebed9c8eef462da2e8398962d3cda441a27c..79d740d04eefcf827ccaf08df2b0e8ed86d35116 100644
--- a/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
+++ b/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
@@ -12,7 +12,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     receives enough service to become nonpreemptive. *)
 Module AbstractRTALockInService. 
 
-  Import Job Epsilon UniprocessorSchedule Service  AbstractRTADefinitions.
+  Import Job UniprocessorSchedule Service  AbstractRTADefinitions.
 
   (* Previously we defined the notion of lock-in service (see limited.schedule.v file). 
      Lock-in service is the amount of service after which a job cannot be preempted until 
diff --git a/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v b/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
index ac20dd718a2b150926a3440b21e91816a7b7b61e..03412a60cabb9561d1154b02074340d9e6d05a38 100644
--- a/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
+++ b/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
@@ -25,7 +25,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     (4) EDF with floating nonpreemptive regions. *)
 Module RTAforConcreteModels.
 
-  Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+  Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
          ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
          RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves NonpreemptiveSchedule
          FullyNonPreemptivePlatform FullyPreemptivePlatform AbstractRTAforEDFwithArrivalCurves.
diff --git a/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v b/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
index a23e31d5dcdabbc8298bdb3204435a059fc07887..c9ee30e43d40e41f657d4167f4a26403f57bafc0 100644
--- a/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
+++ b/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
@@ -21,7 +21,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
 (** In this module we prove a general RTA theorem for EDF-schedulers. *)
 Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
 
-  Import Epsilon Job ArrivalCurves TaskArrival Priority  UniprocessorSchedule Workload Service
+  Import Job ArrivalCurves TaskArrival Priority  UniprocessorSchedule Workload Service
          ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform RBF 
          AbstractRTAforEDFwithArrivalCurves BusyIntervalJLFP PriorityInversionIsBounded. 
 
diff --git a/model/schedule/uni/limited/edf/response_time_bound.v b/model/schedule/uni/limited/edf/response_time_bound.v
index be6856919e75b71e1fca0086741204137c6ed3ea..0ff63e7b401588ecdc489eed1f13185e91c7377b 100644
--- a/model/schedule/uni/limited/edf/response_time_bound.v
+++ b/model/schedule/uni/limited/edf/response_time_bound.v
@@ -24,7 +24,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     EDF uniprocessor scheduling of real-time tasks with arbitrary arrival models.  *)
 Module AbstractRTAforEDFwithArrivalCurves.
   
-  Import Job Epsilon ArrivalCurves TaskArrival ScheduleOfTask Priority
+  Import Job ArrivalCurves TaskArrival ScheduleOfTask Priority
          UniprocessorSchedule Workload Service ResponseTime MaxArrivalsWorkloadBound
          BusyIntervalJLFP LimitedPreemptionPlatform RBF Service JLFPInstantiation.
  
diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
index 9c75772c1ee124bd7e32096fef6f6595801750d3..8eef99ccc10bfe769c163aa510078a013db3e2a3 100644
--- a/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
+++ b/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
@@ -24,7 +24,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     (4) FP with floating nonpreemptive regions. *)
 Module RTAforConcreteModels.
 
-  Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+  Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
          ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
          RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves NonpreemptiveSchedule
          FullyNonPreemptivePlatform FullyPreemptivePlatform.
diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
index 1d917819387d09eea134ff5d1ec2c674c7fe9505..d5d27a160308e5d5a97d9398faabe9c6b0a9ec2d 100644
--- a/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
+++ b/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
@@ -21,7 +21,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
 (** In this module we prove a general RTA theorem for FP-schedulers *)
 Module RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
 
-  Import Epsilon Job ArrivalCurves TaskArrival Priority  UniprocessorSchedule Workload Service
+  Import Job ArrivalCurves TaskArrival Priority  UniprocessorSchedule Workload Service
          ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform RBF
          AbstractRTAforFPwithArrivalCurves BusyIntervalJLFP PriorityInversionIsBounded. 
 
diff --git a/model/schedule/uni/limited/fixed_priority/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/response_time_bound.v
index 58c43350a70a77c60e44881c4f9c63e8d1c7ccc5..12a68413e0123dcbc5cc4ec98adc0820718194b6 100644
--- a/model/schedule/uni/limited/fixed_priority/response_time_bound.v
+++ b/model/schedule/uni/limited/fixed_priority/response_time_bound.v
@@ -25,7 +25,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     FP uniprocessor scheduling of real-time tasks with arbitrary arrival models.  *)
 Module AbstractRTAforFPwithArrivalCurves.
    
-  Import Epsilon Job ArrivalCurves TaskArrival Priority ScheduleOfTask
+  Import Job ArrivalCurves TaskArrival Priority ScheduleOfTask
          UniprocessorSchedule Workload Service ResponseTime MaxArrivalsWorkloadBound
          LimitedPreemptionPlatform RBF BusyIntervalJLFP JLFPInstantiation.
   
diff --git a/model/schedule/uni/limited/platform/definitions.v b/model/schedule/uni/limited/platform/definitions.v
index a355e2e4419059fa0d77978839fa634711706bda..c9ceedfe314e3ff057e681090bd3182622287f26 100644
--- a/model/schedule/uni/limited/platform/definitions.v
+++ b/model/schedule/uni/limited/platform/definitions.v
@@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
    predicate for various preemption models. *)
 Module LimitedPreemptionPlatform.
 
-  Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority Service.
+  Import Job SporadicTaskset UniprocessorSchedule Priority Service.
   
   (* In this section, we define a processor platform with limited preemptions. *)
   Section Properties.
diff --git a/model/schedule/uni/limited/platform/limited.v b/model/schedule/uni/limited/platform/limited.v
index 0e6dd92b7fc3b1ca0e706ec1d24e49f3e55d1515..dfd07a387a0fcc9931a17be6195a9300a3d67a0a 100644
--- a/model/schedule/uni/limited/platform/limited.v
+++ b/model/schedule/uni/limited/platform/limited.v
@@ -13,7 +13,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
     model with floating nonpreemptive regions. *)
 Module ModelWithLimitedPreemptions.
 
-  Import Epsilon Job NondecreasingSequence UniprocessorSchedule LimitedPreemptionPlatform.
+  Import Job NondecreasingSequence UniprocessorSchedule LimitedPreemptionPlatform.
 
   (* In this section, we instantiate can_be_preempted for the model with fixed preemption points and
      the model with floating nonpreemptive regions. We also prove that the definitions are correct. *)
diff --git a/model/schedule/uni/limited/platform/nonpreemptive.v b/model/schedule/uni/limited/platform/nonpreemptive.v
index 6296c0a8da595c4d8dcf5aa6d9d48a7c638d542f..28db0113204721eb4ebdba6d998b041b730c83b5 100644
--- a/model/schedule/uni/limited/platform/nonpreemptive.v
+++ b/model/schedule/uni/limited/platform/nonpreemptive.v
@@ -17,7 +17,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
    can_be_preempted for the fully nonpreemptive model and prove its correctness. *)
 Module FullyNonPreemptivePlatform.
 
-  Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority
+  Import Job SporadicTaskset UniprocessorSchedule Priority
          Service LimitedPreemptionPlatform.
   
   Section FullyNonPreemptiveModel.
diff --git a/model/schedule/uni/limited/platform/preemptive.v b/model/schedule/uni/limited/platform/preemptive.v
index 5f3d24aad671df86b974e4a4b02b36dd5fad4dec..83ea02c82501e8fb8f3ea9aea78095acc67fc9ce 100644
--- a/model/schedule/uni/limited/platform/preemptive.v
+++ b/model/schedule/uni/limited/platform/preemptive.v
@@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
    can_be_preempted for the fully preemptive model and prove its correctness. *)
 Module FullyPreemptivePlatform.
 
-  Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority
+  Import Job SporadicTaskset UniprocessorSchedule Priority
          Service LimitedPreemptionPlatform.
   
   Section FullyPreemptiveModel.
diff --git a/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v b/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
index 4f84902b3fddbdccdde981d0929440e91e87af9b..35dce5a9e4004b8c549f67d34ff28b94ab832ae8 100644
--- a/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
+++ b/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
@@ -15,7 +15,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     is bounded. *)
 Module PriorityInversionIsBounded.
 
-  Import Epsilon Job Priority UniprocessorSchedule LimitedPreemptionPlatform BusyIntervalJLFP. 
+  Import Job Priority UniprocessorSchedule LimitedPreemptionPlatform BusyIntervalJLFP. 
 
   Section PriorityInversionIsBounded.
 
diff --git a/model/schedule/uni/limited/schedule.v b/model/schedule/uni/limited/schedule.v
index a8825aa75392bda44468f610f93e37ffe4df0933..f09ea867cc6ed6e20e7ea132cc824ec8f1325a6c 100644
--- a/model/schedule/uni/limited/schedule.v
+++ b/model/schedule/uni/limited/schedule.v
@@ -7,7 +7,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* In this file, we provide additional definitions and 
    lemmas about lock-in-serivce-compliant schedules. *)
-  Import Job Epsilon Service UniprocessorSchedule.
+  Import Job Service UniprocessorSchedule.
 
   Section Definitions.
 
diff --git a/restructuring/behavior/job.v b/restructuring/behavior/job.v
index 9f0f973204723b4b18bad5b7024a9cd010480360..e00cd320e70ca029f620a1d6f21589320f276a3d 100644
--- a/restructuring/behavior/job.v
+++ b/restructuring/behavior/job.v
@@ -1,21 +1,17 @@
 From rt.restructuring.behavior Require Export time.
-From mathcomp Require Export eqtype.
+From mathcomp Require Export eqtype ssrnat.
 
 (* Throughout the library we assume that jobs have decidable equality *)
-
 Definition JobType := eqType.
 
 (* Definition of a generic type of parameter relating jobs to a discrete cost *)
-
 Class JobCost (J : JobType) := job_cost : J -> duration.
 
 (* Definition of a generic type of parameter for job_arrival *)
-
 Class JobArrival (J : JobType) := job_arrival : J -> instant.
 
 (* Definition of a generic type of parameter relating jobs to an absolute deadline *)
 Class JobDeadline (J : JobType) := job_deadline : J -> instant.
 
 (* Definition of a generic type of release jitter parameter. *)
-Class JobJitter (J : JobType) := job_jitter : J -> duration.
-
+Class JobJitter (J : JobType) := job_jitter : J -> duration.
\ No newline at end of file
diff --git a/restructuring/model/job.v b/restructuring/model/job.v
new file mode 100644
index 0000000000000000000000000000000000000000..ba5d58e509a8abea00fb293d504acd1d4878fdcf
--- /dev/null
+++ b/restructuring/model/job.v
@@ -0,0 +1,17 @@
+From rt.restructuring.behavior Require Export time job.
+From mathcomp Require Export eqtype ssrnat.
+
+(* In this section, we introduce properties of a job. *)
+Section PropertesOfJob.
+
+  (* Assume that job costs are known. *)
+  Context {Job : JobType}.
+  Context `{JobCost Job}.
+
+  (* Consider an arbitrary job. *)
+  Variable j: Job.
+
+  (* The job cost must be positive. *)
+  Definition job_cost_positive := job_cost j > 0.
+
+End PropertesOfJob.
\ No newline at end of file
diff --git a/restructuring/model/schedule/priority_based/preemptive.v b/restructuring/model/schedule/priority_based/preemptive.v
index 6eece44ef67a1ea849dfcee1bc382fa33aea9009..c8d265402d14ef11b13f4b2d4c0d93debe71c65a 100644
--- a/restructuring/model/schedule/priority_based/preemptive.v
+++ b/restructuring/model/schedule/priority_based/preemptive.v
@@ -25,4 +25,5 @@ Section Priority.
       backlogged sched j t ->
       scheduled_at sched j_hp t ->
       hep_job_at t j_hp j.
+  
 End Priority.
diff --git a/restructuring/model/schedule/sequential.v b/restructuring/model/schedule/sequential.v
index bbbddef03ec512c7e4be9cc9eb45a511fb09bd75..664414f6dec1aa7dae10368683772ccfc80dbfde 100644
--- a/restructuring/model/schedule/sequential.v
+++ b/restructuring/model/schedule/sequential.v
@@ -2,9 +2,10 @@ From rt.restructuring.behavior Require Export schedule.
 From rt.restructuring.model Require Export task.
 
 Section PropertyOfSequentiality.
+
   (* Consider any type of job associated with any type of tasks... *)
-  Context {Job: JobType}.
-  Context {Task: TaskType}.
+  Context {Job : JobType}.
+  Context {Task : TaskType}.
   Context `{JobTask Job Task}.
 
   (* ... with arrival times and costs ... *)
diff --git a/restructuring/model/schedule/task_schedule.v b/restructuring/model/schedule/task_schedule.v
new file mode 100644
index 0000000000000000000000000000000000000000..97c6a111e25b91a11f0271d085e0389cec5c326d
--- /dev/null
+++ b/restructuring/model/schedule/task_schedule.v
@@ -0,0 +1,52 @@
+From rt.restructuring.model Require Import task.
+From rt.restructuring.behavior Require Import schedule ideal_schedule.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* Due to historical reasons this file defines the notion of a schedule of 
+   a task for the ideal uniprocessor model. This is not a fundamental limitation
+   and the notion can be further generalized to an arbitrary model. *)
+
+(** * Schedule of task *)
+(** In this section we define properties of schedule of a task *)
+Section ScheduleOfTask.
+ 
+  (* Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (*  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  
+  (* Let sched be any ideal uniprocessor schedule. *)
+  Variable sched : schedule (ideal.processor_state Job).
+
+  Section TaskProperties.
+
+    (* Let tsk be any task. *) 
+    Variable tsk : Task.
+    
+    (* Next we define whether a task is scheduled at time t, ... *)
+    Definition task_scheduled_at (t : instant) :=
+      if sched t is Some j then
+        job_task j == tsk
+      else false.
+
+    (* ...which also corresponds to the instantaneous service it receives. *)
+    Definition task_service_at (t: instant) := task_scheduled_at t.
+
+    (* Based on the notion of instantaneous service, we define the
+       cumulative service received by tsk during any interval [t1, t2)... *)
+    Definition task_service_during (t1 t2 : instant) :=
+      \sum_(t1 <= t < t2) task_service_at t.
+
+    (* ...and the cumulative service received by tsk up to time t2,
+       i.e., in the interval [0, t2). *)
+    Definition task_service (t2 : instant) := task_service_during 0 t2.
+
+  End TaskProperties.
+
+End ScheduleOfTask. 
\ No newline at end of file
diff --git a/restructuring/model/task.v b/restructuring/model/task.v
index f530b004499d9e3fc9154a77e604229c4e940d08..e583ceb74c0389cb2a8b8bd13f45e9af6c1e408a 100644
--- a/restructuring/model/task.v
+++ b/restructuring/model/task.v
@@ -1,15 +1,16 @@
 From mathcomp Require Export ssrbool.
 From rt.restructuring.behavior Require Export job.
 
+From rt.restructuring.behavior Require Export arrival_sequence.
+  
 (* Throughout the library we assume that tasks have decidable equality *)
-
 Definition TaskType := eqType.
 
 (* Definition of a generic type of parameter relating jobs to tasks *)
-
 Class JobTask (J : JobType) (T : TaskType) := job_task : J -> T.
 
 Section SameTask.
+  
   (* For any type of job associated with any type of tasks... *)
   Context {Job: JobType}.
   Context {Task: TaskType}.
@@ -21,12 +22,112 @@ Section SameTask.
 
 End SameTask.
 
+
 (* Definition of a generic type of parameter for task deadlines *)
 Class TaskDeadline (Task : TaskType) := task_deadline : Task -> duration.
 
 (* Given task deadlines and a mapping from jobs to tasks we provide a generic definition of job_deadline *)
-
 Instance job_deadline_from_task_deadline
-        (Job : JobType) (Task : TaskType)
-        `{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} :
-  JobDeadline Job := fun j => job_arrival j + task_deadline (job_task j).
+         (Job : JobType) (Task : TaskType)
+         `{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} : JobDeadline Job :=
+  fun j => job_arrival j + task_deadline (job_task j).
+
+
+(* Definition of a generic type of parameter for task cost *)
+Class TaskCost (T : TaskType) := task_cost : T -> duration.
+
+
+(* In this section, we introduce properties of a task. *)
+Section PropertesOfTask.
+
+  (* Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskDeadline Task}.
+
+  (* Next we intrdoduce attributes of a valid sporadic task. *)
+  Section ValidTask.
+    
+    (* Consider an arbitrary task. *)
+    Variable tsk: Task.
+    
+    (* The cost and deadline of the task must be positive. *)
+    Definition task_cost_positive := task_cost tsk > 0.
+    Definition task_deadline_positive := task_deadline tsk > 0.
+
+    (* The task cost cannot be larger than the deadline or the period. *)
+    Definition task_cost_le_deadline := task_cost tsk <= task_deadline tsk.
+    
+  End ValidTask.
+  
+  (* Job of task *)
+  Section ValidJobOfTask.
+    
+    (* Consider any type of jobs associated with the tasks ... *)
+    Context {Job : JobType}.
+    Context `{JobTask Job Task}.
+    Context `{JobCost Job}.
+    Context `{JobDeadline Job}.
+
+    (* Consider an arbitrary job. *)
+    Variable j: Job.
+
+    (* The job cost cannot be larger than the task cost. *)
+    Definition job_cost_le_task_cost :=
+      job_cost j <= task_cost (job_task j).
+
+  End ValidJobOfTask.
+
+  (* Jobs of task *)
+  Section ValidJobsTask.
+          
+    (* Consider any type of jobs associated with the tasks ... *)
+    Context {Job : JobType}.
+    Context `{JobTask Job Task}.
+    Context `{JobCost Job}.
+    
+    (* ... and any arrival sequence. *)
+    Variable arr_seq : arrival_sequence Job.
+
+    (* The cost of a job from the arrival sequence cannot
+       be larger than the task cost. *)
+    Definition cost_of_jobs_from_arrival_sequence_le_task_cost :=
+      forall j,
+        arrives_in arr_seq j ->
+        job_cost_le_task_cost j.
+
+  End ValidJobsTask.
+
+End PropertesOfTask.
+
+(* In this section, we introduce properties of a task set. *)
+Section PropertesOfTaskSet.
+
+  (* Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (*  ... and any type of jobs associated with these tasks ... *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobCost Job}.
+
+  (* ... and any arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (* Consider an arbitrary task set. *)
+  Variable ts : seq Task.
+
+  (* Tasks from the task set have a positive cost. *)
+  Definition tasks_cost_positive :=
+    forall tsk,
+      tsk \in ts ->
+      task_cost_positive tsk. 
+
+  (* All jobs in the arrival sequence come from the taskset. *)
+  Definition all_jobs_from_taskset :=
+    forall j,
+      arrives_in arr_seq j ->
+      job_task j \in ts.
+
+End PropertesOfTaskSet. 
\ No newline at end of file
diff --git a/restructuring/model/task_arrivals.v b/restructuring/model/task_arrivals.v
index 943bebf34f85202459d9f05ffbb4c224962211ea..1f5905db06d4278c59b6258b42f4485377ec5424 100644
--- a/restructuring/model/task_arrivals.v
+++ b/restructuring/model/task_arrivals.v
@@ -3,15 +3,18 @@ From rt.restructuring.model Require Export task.
 
 (* In this file we provide basic definitions related to tasks on arrival sequences *)
 Section TaskArrivals.
-  Context {Job : JobType} {Task : TaskType}.
 
+  (* Consider any type of job associated with any type of tasks. *)
+  Context {Job: JobType}.
+  Context {Task: TaskType}.
   Context `{JobTask Job Task}.
 
-  (* Consider any job arrival sequence, *)
+  (* Consider any job arrival sequence. *)
   Variable arr_seq: arrival_sequence Job.
 
   Section Definitions.
-    (* And a given task *)
+
+    (* Let tsk be any task. *)
     Variable tsk : Task.
 
     (* We define the sequence of jobs of tsk arriving at time t *)
diff --git a/restructuring/model/task_cost.v b/restructuring/model/task_cost.v
deleted file mode 100644
index 014720c3dba960e2ac90995e3dc4b2b988f0ca3c..0000000000000000000000000000000000000000
--- a/restructuring/model/task_cost.v
+++ /dev/null
@@ -1,35 +0,0 @@
-From rt.restructuring.behavior Require Export arrival_sequence.
-From rt.restructuring.model Require Export task.
-
-Section TaskCost.
-  Context {T : TaskType}.
-
-  Variable (task_cost : duration).
-
-  Definition valid_task_cost := task_cost > 0.
-End TaskCost.
-
-(* Definition of a generic type of parameter for task cost *)
-
-Class TaskCost (T : TaskType) := task_cost : T -> duration.
-
-Section TasksetCosts.
-  Context {T : TaskType} `{TaskCost T}.
-
-  Variable ts : seq T.
-
-  Definition valid_taskset_costs :=
-    forall tsk : T,
-      tsk \in ts ->
-      task_cost tsk > 0.
-
-  Context {J : JobType} `{JobTask J T} `{JobCost J}.
-
-  Variable arr_seq : arrival_sequence J.
-
-  Definition respects_taskset_costs :=
-    forall j,
-      arrives_in arr_seq j ->
-      job_cost j <= task_cost (job_task j).
-
-End TasksetCosts.
diff --git a/util/epsilon.v b/util/epsilon.v
index d66c6b81f9ca62cb9c4a46f54a6657b845572648..dae64637cd4cd8a7a326c82609a45586dc7822e6 100644
--- a/util/epsilon.v
+++ b/util/epsilon.v
@@ -1,4 +1,4 @@
-Module Epsilon.
+Section Epsilon.
 
   (* ε is defined as the smallest positive number. *)
   Definition ε := 1.