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: |
|---|---|---|---|
| ngp-10 | proved | all subs proved | cngetput, |
| eq-put2 | proved | all subs proved | Put-other, Put-same, cputput, Extension, |
| put-put-get-ls | proved | all subs proved | cgetput, |
| putgetinv | proved | all subs proved | eq-write-left, |
| ngp-06 | proved | all subs proved | cngetput, |
| ngp-07 | proved | all subs proved | cngetput, |
| ngp-08 | proved | all subs proved | cngetput, |
| ngp-09 | proved | all subs proved | cngetput, |
| eq-write-1 | proved | all subs proved | Put-same, cngetput, Extension, |
| put-same-content | proved | all subs proved | eq-write-left, |
| write3 | proved | all subs proved | put-put-get-neq, Put-other, Put-same, Extension, |
| put-put-get-neq | proved | all subs proved | Put-same, |
| eq-write-left | proved | all subs proved | Put-other, Put-same, Extension, |
| cgetput | proved | all subs proved | Put-same, |
| cputput | proved | all subs proved | Put-other, Put-same, Extension, |
| cngetput | proved | all subs proved | Put-other, |
| cputput-reverse | proved | all subs proved | Put-same, Put-other, Extension, |
| eq-write-2 | proved | all subs proved | Put-same, Put-other, Extension, |
| ext-rec | proved | all subs proved | Put-other, Put-same, Extension, |
| cngetput-num | proved | all subs proved | Put-other, |
| Extension | axiom | ||
| Put-other | axiom | ||
| Put-same | axiom |