`busy_intervals_are_bounded_by` definition

Currently., the definition of busy_intervals_are_bounded_by has the preconditions: t1 <= job_arrival j < t2, and busy_interval t1 t2. This is an issue since, the latter implies the former.