behavior/schedule/service_facts.v · 7ba4060555b92a34a5889d21b1cfab6bc250452e · Lasse Blaauwbroek / PROSA - Formally Proven Schedulability Analysis

Forked from RT-PROOFS / PROSA - Formally Proven Schedulability Analysis

Source project has a limited visibility.

5 years ago

Port lemmas from model/schedule/uni/schedule.v · 7ba40605

- port completed_implies_scheduled_before
- port lemmas on service prior to arrival
- port scheduled_implies_pending and greatly simplify the proof while at it
- port and simplify job_pending_at_arrival
- port cumulative_service_implies_scheduled and simplify proof of
  positive_service_implies_scheduled_before
- port service_is_a_step_function

7ba40605

History

Port lemmas from model/schedule/uni/schedule.v

Björn Brandenburg authored 5 years ago

- port completed_implies_scheduled_before
- port lemmas on service prior to arrival
- port scheduled_implies_pending and greatly simplify the proof while at it
- port and simplify job_pending_at_arrival
- port cumulative_service_implies_scheduled and simplify proof of
  positive_service_implies_scheduled_before
- port service_is_a_step_function