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: |
|---|---|---|---|
| uninit-eq | proved | all subs proved | uninit, |
| uninit-02 | proved | all subs proved | uninit, |
| uninit-01 | proved | all subs proved | uninit, |
| type-neq | proved | all subs proved | type, |
| type-fieldspec | proved | all subs proved | type, |
| type-12 | proved | all subs proved | type, |
| type-11 | proved | all subs proved | type, |
| type-10 | proved | all subs proved | type, |
| type-09 | proved | all subs proved | type, |
| type-08 | proved | all subs proved | type, |
| type-07 | proved | all subs proved | type, |
| type-06 | proved | all subs proved | type, |
| type-05 | proved | all subs proved | type, |
| type-04 | proved | all subs proved | length, type, |
| type-03 | proved | all subs proved | type, |
| type-02 | proved | all subs proved | type, |
| type-01 | proved | all subs proved | type, |
| th-01 | proved | all subs proved | mode, |
| out-05 | proved | all subs proved | length, out, |
| out-04 | proved | all subs proved | out, |
| out-03 | proved | all subs proved | out, |
| out-02 | proved | all subs proved | out, |
| out-01 | proved | all subs proved | out, |
| mode-ref | proved | all subs proved | mode, |
| mode-neq | proved | all subs proved | mode, |
| mode-key | proved | all subs proved | mode, |
| mode-06 | proved | all subs proved | mode, |
| mode-05 | proved | all subs proved | length, mode, |
| mode-04 | proved | all subs proved | mode, |
| mode-03 | proved | all subs proved | mode, |
| mode-02 | proved | all subs proved | mode, |
| mode-01 | proved | all subs proved | mode, |
| length-diff | proved | all subs proved | length, |
| length-05 | proved | all subs proved | length, |
| length-04 | proved | all subs proved | length, |
| length-03 | proved | all subs proved | length, |
| length-02 | proved | all subs proved | length, |
| length-01 | proved | all subs proved | length, |
| len | proved | all subs proved | length, |
| initfield-01 | proved | all subs proved | initfield, |
| endfin-ref | proved | all subs proved | endfinallymode, |
| endfin-key | proved | all subs proved | endfinallymode, |
| endfin-eq | proved | all subs proved | endfinallymode, |
| endfin-diff-02 | proved | all subs proved | uninit, endfinallymode, |
| endfin-diff-01 | proved | all subs proved | mode, endfinallymode, |
| endfin-diff | proved | all subs proved | out, endfinallymode, |
| diff-07 | proved | all subs proved | uninit, |
| diff-06 | proved | all subs proved | uninit, length, |
| diff-05 | proved | all subs proved | uninit, type, |
| diff-04 | proved | all subs proved | out, uninit, |
| diff-03 | proved | all subs proved | mode, uninit, |
| diff-02 | proved | all subs proved | out, type, |
| diff-01 | proved | all subs proved | mode, type, |
| diff | proved | all subs proved | mode, out, |
| initfield | axiom | ||
| endfinallymode | axiom | ||
| length | axiom | ||
| uninit | axiom | ||
| type | axiom | ||
| out | axiom | ||
| mode | axiom |