A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas
above its position. This means the list is a topological order of the dependency graph.
An entry 'all subs proved' means that all used lemmas are (transitively) proved.
| Name: | Status: | Subs proved? | Used: |
|---|
| negint-le-ceil | proved | all subs proved
| ceil-is-neg-floor-neg,
int-le-ceil,
|
| negint-ls-ceil | proved | all subs proved
| floor-ls-int,
ceil-is-neg-floor-neg,
int-ls-ceil,
|
| int-ls-ceil | proved | all subs proved
| floor-ls-negint,
ceil-is-neg-floor-neg,
|
| int-le-ceil | proved | all subs proved
| floor-le-negint,
ceil-is-neg-floor-neg,
|
| ceil-le-negint | proved | all subs proved
| int-le-floor,
ceil-is-neg-floor-neg,
ceil-le-int,
|
| ceil-ls-negint | proved | all subs proved
| ceil-is-neg-floor-neg,
ceil-ls-int,
|
| ceil-ls-int | proved | all subs proved
| ceil-ls-add-one,
ceil-ge,
ceil-is-neg-floor-neg,
|
| ceil-le-int | proved | all subs proved
| ceil-ls-add-one,
ceil-ge,
ceil-is-neg-floor-neg,
|
| floor-le-negint | proved | all subs proved
| floor-le-int,
|
| floor-ls-negint | proved | all subs proved
| negint-le-floor,
floor-ls-int,
|
| ls-notceilgr | proved | all subs proved
| le-notceilgr,
|
| ceil-addint | proved | all subs proved
| ceil-int,
ceil-triang,
ceil-notls,
ceil-ls-add-one,
|
| ls-notfloorgr | proved | all subs proved
| le-notfloorgr,
|
| le-notfloorgr | proved | all subs proved
| le-floorle,
|
| floor-ls-int | proved | all subs proved
| int-le-floor,
|
| negint-le-floor | proved | all subs proved
| int-le-floor,
|
| ceil-triang | proved | all subs proved
| ceil-notls,
ceil-ls-add-one,
|
| le-notceilgr | proved | all subs proved
| le-ceille,
|
| ceil-is-neg-floor-neg | proved | all subs proved
| floor-le,
ceil-ls-add-one,
ceil-notls,
floor-gr-subone,
|
| floor-le-int | proved | all subs proved
| int-ls-floor,
floor-gr-subone,
|
| negint-ls-floor | proved | all subs proved
| int-ls-floor,
|
| ls-floorle | proved | all subs proved
| le-floorle,
|
| ls-ceille | proved | all subs proved
| le-ceille,
|
| floor-addint | proved | all subs proved
| floor-notls,
floor-gr-subone,
floor-int,
floor-triang,
|
| floor-triang | proved | all subs proved
| floor-gr-subone,
floor-le,
|
| floor-int | proved | all subs proved
| floor-gr-subone,
floor-le,
|
| floor-notls | proved | all subs proved
| floor-le,
|
| int-le-floor | proved | all subs proved
| floor-gr-subone,
floor-le,
|
| ceil-int | proved | all subs proved
| ceil-ls-add-one,
ceil-ge,
|
| le-floorle | proved | all subs proved
| floor-gr-subone,
floor-le,
|
| le-ceille | proved | all subs proved
| ceil-ls-add-one,
ceil-ge,
|
| ceil-notls | proved | all subs proved
| ceil-ge,
|
| int-ls-floor | proved | all subs proved
| floor-gr-subone,
floor-le,
|
| ls-floorsuc | proved | all subs proved
| floor-gr-subone,
|
| gr-ceilpred | proved | all subs proved
| ceil-ls-add-one,
|
| floor-le | axiom | | |
| floor-gr-subone | axiom | | |
| ceil-ge | axiom | | |
| ceil-ls-add-one | axiom | | |