tuned;

discontinued worker_trend: prefer constant number of active + reserve threads; tuned exceptional situations;

tuned;

added lemma

typo

avoid writing into source

clarified active_job: take dependencies into account (e.g. future based on promise);

tuned;

non-strict print_state: display old proof state on failure, e.g. unfinished command;

permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;