Library prosa.analysis.facts.model.offset

In this module, we prove some properties of task offsets.
Section OffsetLemmas.

Consider any type of tasks with an offset ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any arrival sequence with consistent and non-duplicate arrivals ...
... and any job j (that stems from the arrival sequence) of any task tsk with a valid offset.
  Variable tsk : Task.
  Variable j : Job.
  Hypothesis H_job_of_task: job_task j = tsk.
  Hypothesis H_valid_offset: valid_offset arr_seq tsk.
  Hypothesis H_job_from_arrseq: arrives_in arr_seq j.

We show that the if j is the first job of task tsk then j arrives at task_offset tsk.
Consider any task set ts.
  Variable ts : TaskSet Task.

If task tsk is in ts, then its offset is less than or equal to the maximum offset of all tasks in ts.