# Library prosa.analysis.facts.hyperperiod

In this file we prove some simple properties of hyperperiods of periodic tasks.
Section Hyperperiod.

Consider any type of periodic tasks, ...

... any task set ts, ...

Hypothesis H_tsk_in_ts: tsk \in ts.

In this section we show a property of hyperperiod in context of task sets with valid periods.
Consider any type of periodic tasks ...

... and any task set ts ...

... such that all tasks in ts have valid periods.
Hypothesis H_valid_periods: valid_periods ts.

We show that the hyperperiod of task set ts is positive.
In this section we prove some lemmas about the hyperperiod in context of the periodic model.
Section PeriodicLemmas.

Consider any type of tasks, ...

... any type of jobs, ...
Context {Job : JobType}.
Context `{JobArrival Job}.

... and a consistent arrival sequence with non-duplicate arrivals.
Consider a task set ts such that all tasks in ts have valid periods.
Hypothesis H_valid_periods: valid_periods ts.

Let tsk be any periodic task in ts with a valid offset and period.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_valid_period: valid_period tsk.

Assume we have an infinite sequence of jobs in the arrival sequence.
Let O_max denote the maximum task offset in ts and let HP denote the hyperperiod of all tasks in ts.
Let HP := hyperperiod ts.

We show that the job corresponding to any job j1 in any other hyperperiod is of the same task as j1.
We show that if a job j lies in the hyperperiod starting at instant t then j arrives in the interval `[t, t + HP)`.
We show that the number of jobs in a hyperperiod starting at n1 × HP + O_max is the same as the number of jobs in a hyperperiod starting at n2 × HP + O_max given that n1 is less than or equal to n2.
We generalize the above lemma by lifting the condition on n1 and n2.
Consider any two jobs j1 and j2 that stem from the arrival sequence arr_seq such that j1 is of task tsk.
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.