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