Marco Maida authored 2 years ago and Björn Brandenburg committed 2 years ago

- Slightly change `valid_nonpreemptive_readiness` so that `sched` is a
  parameter. This way, the proposition can be assumed to hold only for a
  certain schedule (making weaker assumptions).

- Modify `prev_job_nonpreemptive, to unconditionally get
  `jobs_must_be_ready_to_execute`.
  
- Revise lemmas accordingly.