`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.

The precondition t1 <= job_arrival j < t2 should be removed. It is anticipated that this will break some proofs. As Bjoern suggested, adding busy_interval t1 t2 -> t1 => job_arrival j < t2 to rt_auto might help in fixing these proofs.

mentioned in commit 4307d298

mentioned in merge request !223 (merged)

closed with merge request !223 (merged)

closed with commit 4307d298