# Library prosa.analysis.facts.readiness_interference

Require Export prosa.analysis.definitions.readiness_interference.
Require Export prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.facts.interference.
Require Export prosa.analysis.definitions.service_inversion.readiness_aware.
In this file, we establish facts about readiness interference.
Section ReadinessInterference.
Consider any kind of jobs with arrival times and execution costs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any processor state model.
Context `{PState : ProcessorState Job}.
Consider any notion of job readiness.
Context `{!JobReady Job PState}.
Consider any valid arrival sequence of jobs ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and any valid schedule of the given arrival sequence.
Variable sched : schedule PState.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Allow for any JLFP priority policy.
Context {JLFP : JLFP_policy Job}.
First, note that readiness interference is exclusive of the interference due to other higher-or-equal-priority jobs.
Lemma no_hep_ready_implies_no_another_hep_interference :
∀ j t,
~~ some_hep_job_ready arr_seq sched j t →
~~ another_hep_job_interference arr_seq sched j t.
Next, we observe that readiness interference is exclusive of service inversion.
Lemma no_hep_ready_implies_no_service_inversion :
∀ j t,
~~ some_hep_job_ready arr_seq sched j t →
~~ service_inversion arr_seq sched j t.
End ReadinessInterference.