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: |
|---|---|---|---|
| firstoc | proved | all subs proved | inkeys-n, inone, inapp, empty, |
| inkeys-nc | proved | all subs proved | inkeys-n, |
| lenequal | proved | all subs proved | app, nuni-01, nuni, inkeys-n, ex, inone, unique-r, inapp, |
| in-put | proved | all subs proved | put-yes, inkeys-n, put-no, inapp, inone, put-empty, empty, |
| inkeys-n | proved | all subs proved | incons, inrec, |
| uniquelen | proved | all subs proved | app, nuni-01, nuni, ex, inone, unique-r, inapp, empty, unique-e, |
| unique-01 | proved | all subs proved | inone, unique-r, inapp, empty, unique, |
| unique-03 | proved | all subs proved | nuni-01, nuni, |
| unique-04 | proved | all subs proved | nuni-01, nuni, |
| incons | proved | all subs proved | inapp, |
| unique | proved | all subs proved | unique-r, inone, inapp, unique-e, one, |
| nuni | proved | all subs proved | inone, unique-r, inapp, empty, nuni-01, |
| app | proved | all subs proved | inapp, unique-r, not, |
| insnotin | proved | all subs proved | put-no, inone, inapp, put-empty, |
| in-02 | proved | all subs proved | inone, inapp, |
| in-03 | proved | all subs proved | inapp, |
| insfirst | proved | all subs proved | put-no, inone, inapp, put-yes, |
| unique-02 | proved | all subs proved | in-01, unique-r, |
| copied-inrec | proved | all subs proved | inone, inapp, |
| in | proved | all subs proved | in-01, unique-r, |
| lenle | proved | all subs proved | ex, empty, unique-e, inone, unique-r, inapp, |
| in-01 | proved | all subs proved | inassoc, |
| ex | proved | all subs proved | inassoc, |
| nuni-01 | proved | all subs proved | not, unique-r, |
| inapp | proved | all subs proved | inassoc, |
| inone | proved | all subs proved | inassoc, |
| copied-empty | proved | all subs proved | inassoc, |
| one | proved | all subs proved | unique-e, empty, unique-r, |
| not | proved | all subs proved | unique-r, |
| inassoc | proved | all subs proved | inrec, empty, |
| infirst | proved | all subs proved | inrec, |
| one-01 | proved | all subs proved | assoc-yes, |
| put-one | proved | all subs proved | put-yes, |
| k-unique-r | proved | all subs proved | unique-r, unique-e, |
| assoc-yes | axiom | ||
| inrec | axiom | ||
| put-yes | axiom | ||
| unique-e | axiom | ||
| empty | axiom | ||
| unique-r | axiom | ||
| put-empty | axiom | ||
| put-no | axiom |