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: |
|---|
| rely-persist-W-weak | proved | all subs proved
| take-firstPersistW-filter-FO,
at-firstPersistW-is-W,
weak-write-postfix,
rely-def,
allrely-def,
firstPersistW,
|
| at-firstPersistW-is-W | proved | all subs proved
| firstPersistW,
firstPersistW-base,
|
| firstPersistW-base | proved | all subs proved
| firstPersistW,
|
| take-firstPersistW-filter-FO | proved | all subs proved
| firstPersistW,
|
| rely-fo-follows-w-stable | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
|
| rely-no-event-added-by-other | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
|
| rely-add-other-w | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
|
| rely-refl | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
|
| one-pending-del-persist-FO-no-pending | proved | all subs proved
| isPersistFO,
|
| firstPersistW-lt-filter-W-empty | proved | all subs proved
| firstPersistW,
|
| isPersistFO-leading-W | proved | all subs proved
| isPersistFO,
|
| rely-no-pending-stable | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
|
| isPersistFO-rec | proved | all subs proved
| isPersistFO,
|
| firstPersistW-rec-W | proved | all subs proved
| firstPersistW,
|
| rely-add-other-fo | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
|
| rely-persist-FO-weak | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
isPersistFO,
|
| rely-no-pending-w-stable | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
|
| fo-in-del-firstPersistW | proved | all subs proved
| firstPersistW,
|
| isPersistFO-del-no-W-stable | proved | all subs proved
| isPersistFO,
|
| firstPersistW-rec-FO | proved | all subs proved
| firstPersistW,
|
| rely-one-pending-stable | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
|
| rely-persist | proved | all subs proved
| weak-write-postfix,
rely-def,
allrely-def,
|
| isPersistFO | axiom | | |
| allrely-def | axiom | | |
| rely-def | axiom | | |
| weak-write-postfix | axiom | | |
| firstPersistW | axiom | | |