# Library prosa.analysis.facts.busy_interval.quiet_time

In this module we collect some basic facts about quiet times.

Section Facts.

Consider any kind of jobs...
Context {Job : JobType} `{JobArrival Job} `{JobCost Job}.
... and a JLFP policy defined on these jobs.
Context `{JLFP_policy Job}.
Consider any processor state model.
Context {PState : ProcessorState Job}.

Consider any schedule and arrival sequence.
Variable sched : schedule PState.
Variable arr_seq : arrival_sequence Job.

We prove that 0 is always a quiet time.
Lemma zero_is_quiet_time (j : Job) :
quiet_time arr_seq sched j 0.
Proof. by movejhp ARR HP; rewrite /arrived_before ltn0. Qed.

The fact that there is no carry-in at time instant t trivially implies that t is a quiet time.
Lemma no_carry_in_implies_quiet_time :
j t,
no_carry_in arr_seq sched t
quiet_time arr_seq sched j t.
Proof. by movej t + j_hp ARR HP BEF; apply. Qed.

For convenience in proofs, we restate that by definition there are no quiet times in a busy-interval prefix...
Fact busy_interval_prefix_no_quiet_time :
j t1 t2,
busy_interval_prefix arr_seq sched j t1 t2
( t, t1 < t < t2 ¬ quiet_time arr_seq sched j t).
Proof. by movej t1 t2 [_ [_ [NQT _]]]. Qed.

... and hence also not in a busy interval.
Fact busy_interval_no_quiet_time :
j t1 t2,
busy_interval arr_seq sched j t1 t2
( t, t1 < t < t2 ¬ quiet_time arr_seq sched j t).
Proof. by movej t1 t2 [BIP _]; exact: busy_interval_prefix_no_quiet_time. Qed.

End Facts.