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: |
|---|---|---|---|
| sw | proved | all subs proved | eq-04, |
| one | proved | all subs proved | ne-02, ne-01, In-empty, Extension, in-04, |
| eqtwo | proved | all subs proved | in-04, In-insert, Extension, |
| two-01 | proved | all subs proved | ne-02, ne-01, in-04, Extension, |
| sub-one-01 | proved | all subs proved | ne-02, ne-01, in-04, Extension, In-empty, Subset, |
| eq-06 | proved | all subs proved | eq-04, |
| sub-two | proved | all subs proved | in-04, sub-one-02, sub-add-03, add-01, |
| addtwo | proved | all subs proved | In-insert, eq-04, eq, |
| eqtwo-01 | proved | all subs proved | in-04, add, In-insert, In-empty, eq, Extension, |
| subset | proved | all subs proved | Subset, sub-idem, eq, ne-02, ne-01, sub-add-01, sub-insert, add-01, In-insert, |
| eq-05 | proved | all subs proved | eq-04, |
| eq-02 | proved | all subs proved | ne-02, ne-01, In-empty, Extension, in-04, In-insert, |
| two | proved | all subs proved | eq-04, in-04, In-insert, Extension, |
| in-06 | proved | all subs proved | in-04, |
| sub-insert | proved | all subs proved | sub-add-01, ne-02, ne-01, In-insert, Subset, sub-idem, sub-ntrans, eq, |
| sub-one-02 | proved | all subs proved | sub-e, sub-add-03, |
| in-04 | proved | all subs proved | add, In-empty, in-02, |
| eq-04 | proved | all subs proved | In-insert, ins-two, eq, Extension, |
| subset-ins | proved | all subs proved | In-insert, sub-add-03, sub-add-02, |
| sub-insert-01 | proved | all subs proved | sub-add-01, sub-ntrans, |
| in-03 | proved | all subs proved | add, in-02, |
| eq-subset | proved | all subs proved | subset-equal, sub-idem, |
| ins-two | proved | all subs proved | In-insert, eq-03, |
| subset-equal | proved | all subs proved | ne-02, ne-01, Subset, Extension, |
| in-02 | proved | all subs proved | in, In-insert, |
| sub-ntrans | proved | all subs proved | ne-02, ne-01, Subset, |
| sub-add-02 | proved | all subs proved | ne-02, ne-01, Subset, In-insert, |
| add-01 | proved | all subs proved | In-insert, eq-03, |
| sub-add-03 | proved | all subs proved | ne-02, ne-01, Subset, sub-add, In-insert, |
| sub-ntrans-01 | proved | all subs proved | ne-02, ne-01, Subset, |
| sub-add-04 | proved | all subs proved | ne-02, ne-01, In-insert, Subset, |
| sub-in | proved | all subs proved | ne-02, ne-01, Subset, |
| sel | proved | all subs proved | ne-02, ne-01, In-empty, Extension, |
| sub-trans | proved | all subs proved | ne-02, ne-01, Subset, |
| addthree | proved | all subs proved | In-insert, eq-03, |
| in | proved | all subs proved | add, |
| ne-02 | proved | all subs proved | In-empty, Extension, ne-01, |
| eq-03 | proved | all subs proved | In-insert, Extension, eq, |
| in-01 | proved | all subs proved | add, |
| sub-e | proved | all subs proved | In-empty, Subset, |
| sub-add | proved | all subs proved | Subset, In-insert, |
| sub-idem | proved | all subs proved | Subset, |
| sub-add-01 | proved | all subs proved | In-insert, Subset, |
| add | proved | all subs proved | In-insert, |
| eq | proved | all subs proved | In-insert, Extension, |
| ne-01 | proved | all subs proved | In-empty, |
| in-05 | proved | all subs proved | In-insert, Extension, |
| subset-empty | proved | all subs proved | In-empty, Extension, Subset, |
| sw-01 | proved | all subs proved | In-insert, Extension, |
| expand | proved | all subs proved | construct-set, Extension, gen, |
| ne | proved | all subs proved | In-insert, In-empty, Extension, |
| alle | proved | all subs proved | In-empty, Extension, |
| eq-01 | proved | all subs proved | Extension, In-insert, |
| gen | axiom | ||
| construct-set | axiom | ||
| Subset | axiom | ||
| In-empty | axiom | ||
| Extension | axiom | ||
| In-insert | axiom |