# Library prosa.analysis.facts.busy_interval.quiet_time

Require Export prosa.analysis.definitions.busy_interval.classical.

Require Export prosa.analysis.definitions.carry_in.

Require Export prosa.analysis.definitions.carry_in.

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

Consider any kind of jobs...

... and a JLFP policy defined on these jobs.

Consider any processor state model.

Consider any schedule and arrival sequence.

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 move⇒ jhp ARR HP; rewrite /arrived_before ltn0. Qed.

quiet_time arr_seq sched j 0.

Proof. by move⇒ jhp ARR HP; rewrite /arrived_before ltn0. Qed.

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 move⇒ j t + j_hp ARR HP BEF; apply. Qed.

∀ j t,

no_carry_in arr_seq sched t →

quiet_time arr_seq sched j t.

Proof. by move⇒ j 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 move⇒ j t1 t2 [_ [_ [NQT _]]]. Qed.

∀ 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 move⇒ j t1 t2 [_ [_ [NQT _]]]. Qed.

... and hence also not in a busy interval.