Skip to content

Add lemmas about [service_of_jobs]

Sergey Bozhko requested to merge sbozhko/rt-proofs:new_service_lemmas into master

This MR add some lemmas about service_of_jobs.
Also, the MR removes one spurious dependency on ideal uni-processor. That is, previously file model/service_of_jobs.v imported processor.ideal, which is wrong, since model/service_of_jobs.v assumes no specific model for processor.

Merge request reports