Library prosa.model.job.properties
In this section, we introduce properties of a job.
Assume that job costs are known.
Consider an arbitrary job.
The job cost must be positive.
In the next section, we lift the above property to the level
of arrival sequences.
Consider any type of jobs...
... and the cost associated with each job.
Next, consider any arrival sequence of such jobs.
We say that the arrival sequence has positive job costs if every
job in the sequence has positive cost.
Definition arrivals_have_positive_job_costs :=
∀ j,
arrives_in arr_seq j →
job_cost_positive j.
End PropertiesOfAllJobs.
∀ j,
arrives_in arr_seq j →
job_cost_positive j.
End PropertiesOfAllJobs.