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: |
|---|
| is-aligned-down | proved | all subs proved
| mapped-down-mapped,
down-arrow-buf,
down-arrow-block-def,
|
| down-arrow-size1 | proved | all subs proved
| down-arrow-size,
|
| down-arrow-size0 | proved | all subs proved
| down-arrow-size,
|
| align-down-app-left | proved | all subs proved
| align-down-app-same,
|
| mapped-down-mapped | proved | all subs proved
| down-arrow-buf,
down-arrow-block-def,
|
| down-arrow-size | proved | all subs proved
| down-arrow-def,
|
| align-down-app-same | proved | all subs proved
| down-arrow-buf,
|
| synced-write | proved | all subs proved
| synced,
|
| synced-unmap | proved | all subs proved
| synced,
|
| synced-map | proved | all subs proved
| synced,
|
| synced-down-synced | proved | all subs proved
| down-arrow-buf,
down-arrow-block-def,
down-arrow-def,
synced,
|
| synced-buffered-aligned | proved | all subs proved
| awbuf-inv-def,
synced,
|
| synced-aligned | proved | all subs proved
| synced,
|
| inv-write-unbuf | proved | all subs proved
| awbuf-inv-def,
|
| inv-write-buf-destroy | proved | all subs proved
| awbuf-inv-def,
|
| inv-write-buf | proved | all subs proved
| awbuf-inv-def,
|
| inv-unmap | proved | all subs proved
| awbuf-inv-def,
|
| inv-synced-write-buf | proved | all subs proved
| awbuf-inv-def,
synced,
|
| inv-nobuf-synced | proved | all subs proved
| awbuf-inv-def,
synced,
|
| inv-leb-size | proved | all subs proved
| awbuf-inv-def,
|
| inv-is-aligned-notbuffer | proved | all subs proved
| awbuf-inv-def,
|
| inv-buf-in-vol | proved | all subs proved
| awbuf-inv-def,
|
| inv-aligned-synced | proved | all subs proved
| awbuf-inv-def,
synced,
|
| down-written-not-down-before | proved | all subs proved
| down-arrow-buf,
down-arrow-block-def,
down-arrow-def,
|
| down-written-eq | proved | all subs proved
| down-arrow-block-def,
down-arrow-def,
down-arrow-buf,
|
| down-two-writtes | proved | all subs proved
| down-arrow-buf,
down-arrow-block-def,
down-arrow-def,
|
| down-appended-less | proved | all subs proved
| down-arrow-buf,
down-arrow-block-def,
down-arrow-def,
|
| awbuf-inv-crash | proved | all subs proved
| awbuf-inv-def,
down-arrow-buf,
down-arrow-block-def,
down-arrow-def,
|
| align-down-size-is-aligned | proved | all subs proved
| down-arrow-buf,
|
| align-down-size-eq | proved | all subs proved
| down-arrow-buf,
|
| align-down-mkbuf0 | proved | all subs proved
| down-arrow-buf,
|
| align-down-is-aligned | proved | all subs proved
| down-arrow-buf,
|
| align-down-idempot | proved | all subs proved
| down-arrow-buf,
|
| align-down-eq | proved | all subs proved
| down-arrow-buf,
|
| align-down-elim | proved | all subs proved
| down-arrow-buf,
|
| align-down-append-eq | proved | all subs proved
| down-arrow-buf,
|
| synced | axiom | | |
| down-arrow-def | axiom | | |
| down-arrow-block-def | axiom | | |
| awbuf-inv-def | axiom | | |
| down-arrow-buf | axiom | | |