Library prosa.analysis.facts.model.task_schedule

In this file we provide basic properties related to schedule of a task.
Section TaskSchedule.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

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

Let sched be any ideal uni-processor schedule.
Let tsk be any task.
  Variable tsk : Task.

We show that if a job of task tsk is scheduled at time t, then task tsk is scheduled at time t.
  Lemma job_of_task_scheduled_implies_task_scheduled :
     j t,
      job_of_task tsk j
      scheduled_at sched j t
      task_scheduled_at sched tsk t.

And vice versa, if no job of task tsk is scheduled at time t, then task tsk is not scheduled at time t.
  Lemma job_of_task_scheduled_implies_task_scheduled':
     j t,
      ~~ job_of_task tsk j
      scheduled_at sched j t
      ~~ task_scheduled_at sched tsk t.

End TaskSchedule.