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: |
|---|
| upto-stream | proved | all subs proved
| zeropage-mod-pagesize,
getpage,
getbyte,
stream,
|
| stream-upto | proved | all subs proved
| zeropage-mod-pagesize,
getpage,
getbyte,
stream,
|
| stream-split-partial-lastpage | proved | all subs proved
| zeropage-mod-pagesize,
zerostream-size,
getpage,
getbyte,
stream,
|
| stream-split-lastpage | proved | all subs proved
| zeropage-mod-pagesize,
zerostream-size,
getpage,
getbyte,
stream,
|
| stream-size-from | proved | all subs proved
| getpage,
getbyte,
stream,
|
| stream-size | proved | all subs proved
| getpage,
getbyte,
stream,
|
| stream-empty | proved | all subs proved
| zeropage-mod-pagesize,
getpage,
getbyte,
stream,
|
| stream-at | proved | all subs proved
| getpage,
getbyte,
stream,
|
| iso-unfold | proved | all subs proved
| files-iso,
getpage,
getbyte,
stream,
|
| iso-trans | proved | all subs proved
| getpage,
getbyte,
stream,
files-iso,
|
| iso-sym | proved | all subs proved
| getpage,
getbyte,
stream,
files-iso,
|
| iso-refl | proved | all subs proved
| files-iso,
|
| getbyte-drop-upper | proved | all subs proved
| zeropage-mod-pagesize,
getpage,
getbyte,
|
| getbyte-drop-lower | proved | all subs proved
| getpage,
getbyte,
|
| fill-stream-append | proved | all subs proved
| zerostream-size,
|
| emtpystream-merge-to | proved | all subs proved
| zerostream-size,
|
| emptytream-dist-to | proved | all subs proved
| zerostream-size,
|
| content-write | proved | all subs proved
| getpage,
getbyte,
stream,
|
| content-trunc-exact | proved | all subs proved
| zerostream-size,
getpage,
getbyte,
stream,
|
| content-trunc | proved | all subs proved
| zerostream-size,
getpage,
getbyte,
stream,
|
| content-read | proved | all subs proved
| getbyte,
stream,
getpage,
|
| at-content-stream | proved | all subs proved
| getpage,
getbyte,
stream,
|
| afs-cons-getpage-size | proved | all subs proved
| getpage,
|
| files-iso | axiom | | |
| zeropage-mod-pagesize | proved | all subs proved
| |
| zerostream-size | proved | all subs proved
| |
| stream | axiom | | |
| getbyte | axiom | | |
| getpage | axiom | | |