Add lemmas about [service_of_jobs]

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.

assigned to @bbb

added 1 commit

• 3a624d73 - Add lemmas about [service_of_jobs]

Compare with previous version

Thanks, looks very good! I have just a few minor suggestions and questions.

Sergey, can we get this dealt with soon-ish?

added 45 commits

• 3a624d73...fa41e214 - 40 commits from branch RT-PROOFS:master
• 6d1a54f9 - Introduce notion of total service of jobs
• d67850a4 - Add lemmas about [service_of_jobs]
• 9b9bda6e - tweak comment in aggregate/service_of_jobs.v
• e9d24ecc - tweak comments in analysis/facts/model/service_of_jobs.v
• 60fef11d - add note on ideal uniproc limitation

Compare with previous version

resolved all threads

added 2 commits

• 1d00b1f4 - introduce the notion of "total service of jobs"
• 0bcc4898 - add lemmas about [service_of_jobs]

Compare with previous version

added 3 commits

• b5e717e6 - 1 commit from branch RT-PROOFS:master
• e3757dbb - introduce the notion of "total service of jobs"
• e3567e95 - add lemmas about [service_of_jobs]

Compare with previous version

enabled an automatic merge when the pipeline for e3567e95 succeeds

merged