Library prosa.analysis.definitions.job_properties


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)

Require Export prosa.behavior.all.

In this section, we introduce properties of a job.
Section PropertiesOfJob.

Assume that job costs are known.
  Context {Job : JobType}.
  Context `{JobCost Job}.

Consider an arbitrary job.
  Variable j : Job.

The job cost must be positive.
  Definition job_cost_positive := job_cost j > 0.

End PropertiesOfJob.