Add facts.busy_interval

analysis/facts/carry_in.v → analysis/facts/busy_interval/carry_in.v

 Require Export prosa.analysis.facts.workload.
 Require Export prosa.analysis.definitions.carry_in.
-Require Export prosa.analysis.facts.busy_interval.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.analysis.facts.busy_interval.busy_interval.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import prosa.model.processor.ideal.

analysis/facts/priority_inversion.v → analysis/facts/busy_interval/priority_inversion.v

@@ -4,7 +4,7 @@ Require Export prosa.model.schedule.work_conserving.
 Require Export prosa.analysis.definitions.job_properties.
 Require Export prosa.analysis.definitions.busy_interval.
 Require Export prosa.analysis.facts.model.ideal_schedule.
-Require Export prosa.analysis.facts.busy_interval.
+Require Export prosa.analysis.facts.busy_interval.busy_interval.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.

results/edf/rta/bounded_nps.v

 Require Import prosa.model.priority.edf.
 Require Export prosa.analysis.facts.rbf.
 Require Export prosa.analysis.facts.sequential.
-Require Export prosa.analysis.facts.priority_inversion.
 Require Export prosa.results.edf.rta.bounded_pi.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.

results/edf/rta/bounded_pi.v

 Require Export prosa.analysis.facts.edf.
 Require Export prosa.model.schedule.priority_driven.
-Require Export prosa.analysis.facts.priority_inversion.
-Require Export prosa.analysis.facts.carry_in.
+Require Export prosa.analysis.facts.busy_interval.priority_inversion.
+Require Export prosa.analysis.facts.busy_interval.carry_in.
 Require Export prosa.analysis.definitions.schedulability.
 Require Import prosa.model.priority.edf.
 Require Import prosa.model.task.absolute_deadline.

results/fixed_priority/rta/bounded_nps.v

 Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.analysis.definitions.request_bound_function.
 Require Export prosa.analysis.facts.sequential.
-Require Export prosa.analysis.facts.priority_inversion.
+Require Export prosa.analysis.facts.busy_interval.priority_inversion.
 Require Export prosa.results.fixed_priority.rta.bounded_pi.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)

results/fixed_priority/rta/bounded_pi.v

 Require Export prosa.model.schedule.priority_driven.
-Require Export prosa.analysis.facts.busy_interval.
+Require Export prosa.analysis.facts.busy_interval.busy_interval.
 Require Import prosa.analysis.abstract.ideal_jlfp_rta.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.