# Library prosa.analysis.facts.completes_at

Require Export prosa.analysis.definitions.busy_interval.classical.
Require Export prosa.analysis.facts.model.preemption.
In this file, we prove a few useful lemmas about the completes_at predicate.
Section CompletesAtLemmas.
Consider any type of jobs with a priority relation.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JLFP_policy Job}.
Consider any kind of uniprocessor state model.
Context {PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Consider any arrival sequence with consistent non-duplicate arrivals
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Next, consider any schedule of this arrival sequence ...
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
... where jobs do not execute before their arrival or after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
If a job j completes at time t > 0, then it must have been scheduled at time t - 1.
Lemma scheduled_at_precedes_completes_at :
∀ (j : Job) (t : instant),
t > 0 →
completes_at sched j t →
scheduled_at sched j t.-1.
Next, we show that any job j can be completed at most once.
Lemma job_completes_at_most_once :
∀ (j : Job) (t1 t2 : instant),
\sum_(t1 ≤ t < t2) completes_at sched j t ≤ 1.
At any time t > 0, at most one job satisfying predicate P and arriving before time B can complete.
Lemma only_one_job_completes_at_a_time :
∀ (P : pred Job) (t B : instant),
t > 0 →
\sum_(j <- arrivals_before arr_seq B | P j) completes_at sched j t ≤ 1.
Consider a valid preemption model.
Context `{JobPreemptable Job}.
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
We prove that any completion time is a preemption time.
Lemma completetion_time_is_preemption_time :
∀ (j : Job) (t : instant),
completes_at sched j t →
preemption_time arr_seq sched t.
No higher-or-equal priority job that arrived before the start of a busy-interval prefix can complete during the prefix.
Lemma no_early_hep_job_completes_during_busy_prefix :
∀ (j : Job) (t t1 t2 : instant),
busy_interval_prefix arr_seq sched j t1 t2 →
t1 < t ≤ t2 →
∀ jhp : Job,
(jhp \in arrivals_before arr_seq t1) →
hep_job jhp j →
~~ completes_at sched jhp t.
End CompletesAtLemmas.