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: |
|---|
| write-prepost-partial | proved | all subs proved
| write-inv-stream,
write-inv-others,
write-inv-post,
write-inv-meta,
write-inv-in0,
write-loop-inv,
write-inv-ls,
write-inv-in1,
truncate-inv,
|
| write-prepost | proved | all subs proved
| write-inv-stream,
write-inv-others,
write-inv-post,
write-inv-meta,
write-inv-in0,
write-loop-inv,
write-inv-ls,
write-inv-in1,
truncate-inv,
|
| write-loop-inv | proved | all subs proved
| write-block-inv,
|
| write-inv-post | proved | all subs proved
| write-inv,
write-inv-strong,
write-inv-in0,
write-inv-in1,
write-inv-meta,
|
| write-inv-others | proved | all subs proved
| write-inv-strong,
write-inv-ls,
write-inv-in0,
write-inv-in1,
|
| write-inv-stream | proved | all subs proved
| write-inv,
write-inv-strong,
write-inv-in0,
write-inv-in1,
write-inv-meta,
|
| write-inode-inv | proved | all subs proved
| write-inv-meta,
write-inv-strong,
write-inv-in0,
write-inv-in1,
|
| write-block-inv | proved | all subs proved
| write-inv-strong-rec,
|
| write-inv-ls | proved | all subs proved
| write-inv-strong,
write-inv-in0,
write-inv-in1,
|
| write-inv-meta | proved | all subs proved
| write-inv-strong,
write-inv-in0,
write-inv-in1,
|
| write-inv-in0 | proved | all subs proved
| write-inv-strong,
write-inv-in1,
|
| write-inv-strong-rec | proved | all subs proved
| write-inv-rec,
write-inv-strong,
|
| read-loop-inv | proved | all subs proved
| read-inv-rec,
read-inv-strong,
|
| truncate-inv | proved | all subs proved
| write-inv,
write-inv-strong,
|
| write-inv-rec | proved | all subs proved
| write-inv-strong,
write-inv,
|
| write-inv-in1 | proved | all subs proved
| write-inv-strong,
|
| read-inv-rec | proved | all subs proved
| read-inv,
|
| read-inv-post | proved | all subs proved
| read-inv,
read-inv-strong,
|
| write-inv-strong | axiom | | |
| write-inv | axiom | | |
| read-inv-strong | axiom | | |
| read-inv | axiom | | |