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.