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-notinvkey-unchanged-f | proved | all subs proved
| rely-notinvkey-unchanged,
|
| rely-notinvkey-unchanged | proved | all subs proved
| rely-def,
|
| rely-allslotsfull | proved | all subs proved
| between-def,
allslotsfull-def,
rely-def,
|
| allslotsfull-inc | proved | all subs proved
| between-def,
allslotsfull-def,
|
| rely-refl | proved | all subs proved
| rely-def,
|
| allslotsfull-inctrue | proved | all subs proved
| between-def,
allslotsfull-def,
|
| allslotsfull-init | proved | all subs proved
| between-def,
allslotsfull-def,
|
| allslotsfull-incfalse | proved | all subs proved
| between-def,
allslotsfull-def,
|
| rely-size | proved | all subs proved
| rely-def,
|
| rely-trans | proved | all subs proved
| rely-def,
|
| rely-notinvkey-f | proved | all subs proved
| rely-def,
|
| htok-add | proved | all subs proved
| between-def,
allslotsfull-def,
htok-def,
|
| rely-add | proved | all subs proved
| rely-def,
|
| allslotsfull-final-close | proved | all subs proved
| between-def,
allslotsfull-def,
|
| allslotsfull-final | proved | all subs proved
| between-def,
allslotsfull-def,
|
| htok-returnfalse-f | proved | all subs proved
| between-def,
allslotsfull-def,
htok-def,
|
| allslotsfull-iterate | proved | all subs proved
| between-def,
allslotsfull-def,
|
| hash-ok-lem | proved | all subs proved
| hash-ok,
|
| hash-ok | axiom | | |
| htok-def | axiom | | |
| rely-def | axiom | | |
| allslotsfull-def | axiom | | |
| between-def | axiom | | |