Update

Fix a typo and note Pierre Roux's comment on disjuctions vs inductives.

See also: RT-PROOFS/rt-proofs#54 (comment 42229)

In anticipation of future reorganization efforts by Sophie, there's no
point in keeping the two kinds of definitions separate.

Move everything into the new namespace starting with 'prosa' rather
than the bland 'rt'.

The main restructuring thrust is nearing completion, so let's get rid
of the `restructuring` namespace.

improve comments, fix names, move some stuff around

spell checker: add 'supremum' to dictionary

...and define a job's total suspension time.

For improved parallelism and nicer documentation.

This is not yet the final organization, but already an improvement.

Move main high-level results to separate top-level `results` module.
Rationale: Let's make it very clear where to find the main, high-level
results in Prosa, and at the same time let's declutter the analysis
namespace.

Other notable change, apart from moving files around:

- move two key analysis definitions to analysis.definitions
- split RBF definition and facts into separate files
- move facts about ideal schedule to ideal_schedule.v

While at it, clean up some Markdown rendering issues on Gitlab.

Job-level definitions should not depend on task-related modules.

The notion of a valid preemption model for *jobs* should
not depend on any task abstraction. Split the two notions.

This is a purely accidental dependency; purge it.

With proper re-exports everywhere, this is no longer necessary.

The two concepts are tightly coupled and it does not make sense
to mix and match them. Therefore, it's cleaner and easier to
understand if both aspects of the preemption model are instantiated
in the same module next to each other.

No need to keep the two separate as they are tightly coupled anyway,
and the joint file doesn't become too long.

The property is a noun: a model of task sequentiality.

All "kinds of schedules" and associated validity conditions are being
collected in model.schedule.

EDF is defined in terms of jobs, whether or not those jobs stem from
tasks. Make sure our definition is general enough to capture the
possibility of a set of jobs without associated tasks scheduled by
EDF.

The Prosa notion of priority-driven scheduling depends on the
preemption model. That is ok; any theory that doesn't want to deal
with non-preemptive sections can simply Require Export the fully
preemptive model and be done with it.

With this patch, the model module is finally completely independent of
any definitions or proofs in the analysis module.

Move proof of readiness model property to analysis module.

By our newly adopted convention, the model/ module should not depend on analysis facts.

Related issue: #37

Now that we have non-ambiguous dependencies, parallel builds should
work without issue.

This fixes all warnings about ambiguous module names and resolves #49.

It also highlights that we still need to cut down on superfluous
Require Import commands in recently ported files.

...and "Defined" can end one.

This can be useful for learning / teaching.

Add instantiations of aRTA for
(1) fully preemptive,
(2) fully non-preemptive,
(3) limited preemptions,
(4) and floating non-preemptive regions EDF models

Add instantiations of aRTA for
(1) fully preemptive,
(2) fully non-preemptive,
(3) limited preemptions,
(4) and floating non-preemptive regions FP models