Changes

Summary

1. merged
2. One new (necessary) theorem
3. merged
4. more operations to support management of jobs, e.g. from external database;
5. more uniform operations;
6. more operations;
7. clarified signature: more robust;
8. more operations;
9. allow arbitrary info, e.g. for custom scheduler;
10. clarified signature;