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: |
|---|---|---|---|
| all-classes | proved | all subs proved | all-classes-01, |
| all-classes-01 | proved | all subs proved | all-classes-02, |
| type-at | proved | all subs proved | lookup-if, |
| lookup-put-mode | proved | all subs proved | lookup-if, |
| look-type | proved | all subs proved | lookup-if, |
| look-out-01 | proved | all subs proved | lookup-if, |
| look-out | proved | all subs proved | lookup-if, |
| look-ins-01 | proved | all subs proved | lookup-if, |
| look-ins | proved | all subs proved | lookup-if, |
| look-del | proved | all subs proved | look-del-01, |
| length-at | proved | all subs proved | lookup-if, |
| endfinmode-in | proved | all subs proved | sk, |
| at-other-type-10 | proved | all subs proved | lookup-if, |
| at-other-type-09 | proved | all subs proved | lookup-if, |
| at-other-type-08 | proved | all subs proved | lookup-if, |
| at-other-type-07 | proved | all subs proved | lookup-if, |
| at-other-type-06 | proved | all subs proved | lookup-if, |
| at-other-type-05 | proved | all subs proved | lookup-if, |
| at-other-type-04 | proved | all subs proved | lookup-if, |
| at-other-type-03 | proved | all subs proved | lookup-if, |
| at-other-type-02 | proved | all subs proved | lookup-if, |
| at-other-type-01 | proved | all subs proved | lookup-if, |
| at-other-type | proved | all subs proved | lookup-if, |
| at-other-field | proved | all subs proved | lookup-if, |
| at-other-class-01 | proved | all subs proved | lookup-if, |
| at-other-class | proved | all subs proved | lookup-if, |
| at-other-51 | proved | all subs proved | lookup-if, |
| at-other-50 | proved | all subs proved | lookup-if, |
| at-other-49 | proved | all subs proved | lookup-if, |
| at-other-48 | proved | all subs proved | lookup-if, |
| at-other-47 | proved | all subs proved | lookup-if, |
| at-other-46 | proved | all subs proved | lookup-if, |
| at-other-45 | proved | all subs proved | lookup-if, |
| at-other-44 | proved | all subs proved | lookup-if, |
| at-other-43 | proved | all subs proved | lookup-if, |
| at-other-42 | proved | all subs proved | lookup-if, |
| at-other-41 | proved | all subs proved | lookup-if, |
| at-other-40 | proved | all subs proved | lookup-if, |
| at-other-39 | proved | all subs proved | lookup-if, |
| at-other-38 | proved | all subs proved | lookup-if, |
| at-other-37 | proved | all subs proved | lookup-if, |
| at-other-36 | proved | all subs proved | lookup-if, |
| at-other-35 | proved | all subs proved | lookup-if, |
| at-other-34 | proved | all subs proved | lookup-if, |
| at-other-33 | proved | all subs proved | lookup-if, |
| at-other-32 | proved | all subs proved | lookup-if, |
| at-other-31 | proved | all subs proved | lookup-if, |
| at-other-30 | proved | all subs proved | lookup-if, |
| at-other-29 | proved | all subs proved | lookup-if, |
| at-other-28 | proved | all subs proved | lookup-if, |
| at-other-27 | proved | all subs proved | lookup-if, |
| at-other-26 | proved | all subs proved | lookup-if, |
| at-other-25 | proved | all subs proved | lookup-if, |
| at-other-24 | proved | all subs proved | lookup-if, |
| at-other-23 | proved | all subs proved | lookup-if, |
| at-other-22 | proved | all subs proved | lookup-if, |
| at-other-21 | proved | all subs proved | lookup-if, |
| at-other-20 | proved | all subs proved | lookup-if, |
| at-other-19 | proved | all subs proved | lookup-if, |
| at-other-18 | proved | all subs proved | lookup-if, |
| at-other-17 | proved | all subs proved | lookup-if, |
| at-other-16 | proved | all subs proved | lookup-if, |
| at-other-15 | proved | all subs proved | lookup-if, |
| at-other-14 | proved | all subs proved | lookup-if, |
| at-other-13 | proved | all subs proved | lookup-if, |
| at-other-12 | proved | all subs proved | lookup-if, |
| at-other-11 | proved | all subs proved | lookup-if, |
| at-other-10 | proved | all subs proved | lookup-if, |
| at-other-09 | proved | all subs proved | lookup-if, |
| at-other-08 | proved | all subs proved | lookup-if, |
| at-other-07 | proved | all subs proved | lookup-if, |
| at-other-06 | proved | all subs proved | lookup-if, |
| at-other-05 | proved | all subs proved | lookup-if, |
| at-other-04 | proved | all subs proved | lookup-if, |
| at-other-03 | proved | all subs proved | lookup-if, |
| at-other-02 | proved | all subs proved | lookup-if, |
| at-other-01 | proved | all subs proved | lookup-if, |
| at-other | proved | all subs proved | lookup-if, |
| at-mode | proved | all subs proved | lookup-if, |
| look-del-01 | proved | all subs proved | |
| sk | proved | all subs proved | |
| lookup-if | proved | all subs proved | |
| all-classes-02 | proved | all subs proved |