Changes

Summary

1. merged
2. proper Nodes.init (amending 9b35c1171d9a);
3. unused;
4. tuned;
5. clarified signature defaults;
6. clarified types: support a variety of Build_Job instances;
7. clarified signature: more explicit synchronized operations;
8. clarified signature: more explicit synchronized operations;
9. clarified modules (again); clarified signature: idempotent "finish" operation, analogous to "join";
10. clarified signature: more explicit synchronized operations;
11. clarified signature: more explicit synchronized operations;
12. more robust: first register job, then start job;
13. clarified signature: proper scope of synchronized operation;
14. proper synchronized access to mutable state, to support concurrency eventually;
15. tuned signature: explicit marker for mutable global state;
16. tuned;
17. more robust;
18. clarified signature;
19. clarified modules;
20. merged
21. Tidied some really messy proofs
22. added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO