Apply 6 suggestion(s) to 1 file(s)

Co-authored-by: Björn Brandenburg <bbb@mpi-sws.org>

analysis/facts/model/ideal_uni_exceed.v

@@ -24,9 +24,9 @@ Section ExceedanceProcStateProperties.
   (** A job [j] is said to be [scheduled_at] some time [t] if and only if the
       processor state at that time is [NominalExecution j] or
       [ExceedanceExecution j]. *)
-   Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t:
-    scheduled_at sched j t <->
-      sched t = NominalExecution j \/ sched t = ExceedanceExecution j.
+   Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t :
+     scheduled_at sched j t <->
+       sched t = NominalExecution j \/ sched t = ExceedanceExecution j.
   Proof.
     split.
     -  move => SCHED.
@@ -46,7 +46,7 @@ Section ExceedanceProcStateProperties.
 
 
   (** Next we prove that the processor model under consideration is a uniprocessor
-      model i.e., only one job can be scheduled at any time instant. *)
+      model, i.e., only one job can be scheduled at any time instant. *)
   Lemma eps_is_uniproc : uniprocessor_model (exceedance_proc_state Job).
   Proof.
     rewrite /uniprocessor_model.
@@ -63,7 +63,7 @@ Section ExceedanceProcStateProperties.
   Qed.
 
   (** Next, we prove that the processor model under consideration is fully
-      consuming i.e., all the supply offered is consumed by the scheduled job. *)
+      consuming, i.e., all the supply offered is consumed by the scheduled job. *)
   Lemma eps_is_fully_consuming :
     fully_consuming_proc_model (exceedance_proc_state Job).
   Proof.
@@ -81,7 +81,7 @@ Section ExceedanceProcStateProperties.
   Qed.
 
   (** Finally we prove that the processor model under consideration is unit
-      service i.e., it provides at most one unit of service at any time instant. *)
+      service, i.e., it provides at most one unit of service at any time instant. *)
   Lemma eps_is_unit_service : unit_service_proc_model (exceedance_proc_state Job).
   Proof.
     rewrite /unit_service_proc_model.
@@ -97,7 +97,7 @@ End ExceedanceProcStateProperties.
     ideal uniprocessor with exceedance processor state. *)
 Section ExceedanceProcStateProperties1.
 
-  (** In this section we consider any type of jobs. *)
+  (** In this section, we consider any type of jobs. *)
   Context `{Job : JobType}.
 
   (** First let us define the notion of exceedance execution. A processor state
@@ -105,8 +105,8 @@ Section ExceedanceProcStateProperties1.
       [ExceedanceExecution j] for some [j]. *)
   Definition is_exceedance_exec (pstate : (exceedance_proc_state Job)) :=
     match pstate with
-    |ExceedanceExecution _ => true
-    |_ => false
+    | ExceedanceExecution _ => true
+    | _ => false
     end.
   Local Transparent scheduled_in scheduled_on service_on.