Skip to content
  • Björn Brandenburg's avatar
    Port lemmas from model/schedule/uni/schedule.v · 7ba40605
    Björn Brandenburg authored
    - 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