There's now also a `findP` in ssreflect's seq library.

add lemmas on consistency of backlogged jobs set

add notion of a non-clairvoyant readiness model

This is a general definition and not specific to a particular
implementation.

...by adding the -projection-no-head-constant flag to the build settings.

Vedant Chavda authored 4 years ago and Björn Brandenburg committed 4 years ago

change it to perm_big

Added the proof of correctness of the work-conservation transformation for an ideal uniprocessor schedule.