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: |
|---|
| size-0-w | proved | all subs proved
| eq-write-left,
width-put,
gen,
width-mkcube,
height-mkcube,
depth-mkcube,
extension,
|
| cputput-reverse-h | proved | all subs proved
| eq-write-2-h,
|
| cputput-reverse-d | proved | all subs proved
| eq-write-2-d,
|
| size-0-d | proved | all subs proved
| eq-write-left,
depth-put,
gen,
width-mkcube,
height-mkcube,
depth-mkcube,
extension,
|
| size-0-h | proved | all subs proved
| eq-write-left,
height-put,
gen,
width-mkcube,
height-mkcube,
depth-mkcube,
extension,
|
| cputput-reverse-w | proved | all subs proved
| eq-write-2-w,
|
| eq-write-2-w | proved | all subs proved
| put-otherdepth,
put-otherheight,
ngp-07-w,
put-same,
put-otherwidth,
height-put,
depth-put,
width-put,
extension,
|
| eq-write-2-d | proved | all subs proved
| put-otherheight,
put-otherwidth,
ngp-07-w,
put-same,
put-otherdepth,
height-put,
depth-put,
width-put,
extension,
|
| eq-write-2-h | proved | all subs proved
| put-otherdepth,
put-otherwidth,
ngp-07-w,
put-same,
put-otherheight,
height-put,
depth-put,
width-put,
extension,
|
| eq-write-left | proved | all subs proved
| putgetinv,
ngp-07-h,
ngp-07-d,
ngp-07-w,
put-same,
height-put,
depth-put,
width-put,
extension,
|
| eq-write-1 | proved | all subs proved
| ngp-07-h,
ngp-07-d,
ngp-07-w,
put-same,
height-put,
depth-put,
width-put,
extension,
|
| ngp-07-d | proved | all subs proved
| cngetput-d,
|
| ngp-07-h | proved | all subs proved
| cngetput-h,
|
| ngp-07-w | proved | all subs proved
| cngetput-w,
|
| ngp-06-d | proved | all subs proved
| cngetput-d,
|
| ngp-10-wh | proved | all subs proved
| cngetput-w,
|
| ngp-06-h | proved | all subs proved
| cngetput-h,
|
| ngp-08-d | proved | all subs proved
| cngetput-d,
|
| ngp-10-wd | proved | all subs proved
| cngetput-w,
|
| ngp-08-h | proved | all subs proved
| cngetput-h,
|
| put-other | proved | all subs proved
| put-otherheight,
put-otherwidth,
cngetput-d,
|
| ngp-10-dh | proved | all subs proved
| cngetput-d,
|
| ngp-06-w | proved | all subs proved
| cngetput-w,
|
| put-same-content | proved | all subs proved
| extension,
putgetinv,
|
| ngp-08-w | proved | all subs proved
| cngetput-w,
|
| ngp-09-d | proved | all subs proved
| cngetput-d,
|
| ngp-09-h | proved | all subs proved
| cngetput-h,
|
| eq-put2 | proved | all subs proved
| put-otherheight,
put-otherdepth,
put-otherwidth,
put-same,
cputput,
height-put,
depth-put,
width-put,
extension,
|
| ngp-10-h | proved | all subs proved
| cngetput-h,
|
| ngp-10-w | proved | all subs proved
| cngetput-w,
|
| ngp-09-w | proved | all subs proved
| cngetput-w,
|
| ngp-10-d | proved | all subs proved
| cngetput-d,
|
| cputput | proved | all subs proved
| put-otherdepth,
put-otherheight,
put-otherwidth,
put-same,
height-put,
depth-put,
width-put,
extension,
|
| putgetinv | proved | all subs proved
| put-otherdepth,
put-otherheight,
put-otherwidth,
put-same,
height-put,
depth-put,
width-put,
extension,
|
| cngetput-h | proved | all subs proved
| put-otherheight,
|
| cngetput-w | proved | all subs proved
| put-otherwidth,
|
| cngetput-d | proved | all subs proved
| put-otherdepth,
|
| cngetput-num-h | proved | all subs proved
| put-otherheight,
|
| write3 | proved | all subs proved
| put-otherdepth,
put-otherheight,
put-otherwidth,
put-same,
height-put,
depth-put,
width-put,
extension,
|
| cngetput-num-d | proved | all subs proved
| put-otherdepth,
|
| cngetput-num-w | proved | all subs proved
| put-otherwidth,
|
| ext-rec | proved | all subs proved
| put-otherheight,
put-otherdepth,
put-otherwidth,
put-same,
height-put,
depth-put,
width-put,
extension,
|
| depth-mkcube | axiom | | |
| height-mkcube | axiom | | |
| width-mkcube | axiom | | |
| gen | axiom | | |
| extension | axiom | | |
| width-put | axiom | | |
| depth-put | axiom | | |
| height-put | axiom | | |
| put-same | axiom | | |
| put-otherwidth | axiom | | |
| put-otherheight | axiom | | |
| put-otherdepth | axiom | | |