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: |
|---|
| ubifs-dir-data | proved | all subs proved
| ubifs-file-in,
ubifs-file-notdir,
|
| datanode-pagesize | proved | all subs proved
| datakey-cons,
node-closed,
log-cons,
ri-closed,
ri-cons,
ubifs-cons,
ubifs-file-in,
ubifs-file-notdir,
|
| ubifs-file-in | proved | all subs proved
| datanode-closed,
datakey-cons,
log-cons,
ri-closed,
ri-cons,
ubifs-cons,
ubifs-file-notdir,
|
| ubifs-parent-dir | proved | all subs proved
| dentrynode-closed,
dentrykey-cons,
inodenode-closed,
inodekey-cons,
log-cons,
ri-closed,
ri-cons,
ubifs-cons,
ubifs-parent-in,
|
| ubifs-cons-notin-dels | proved | all subs proved
| ubifs-adr-in-ri,
|
| ubifs-cons-notin-del | proved | all subs proved
| ubifs-adr-in-ri,
|
| log-cons-copy-new | proved | all subs proved
| key-cons,
key-node-cons,
log-cons,
ri-cons,
|
| ubifs-parent-in | proved | all subs proved
| dentrynode-closed,
dentrykey-cons,
log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-adr-in-ri | proved | all subs proved
| ubifs-in-fs,
|
| key-node-cons | proved | all subs proved
| dentrykey-cons,
datakey-cons,
inodekey-cons,
node-cons,
|
| ubifs-file-notdir | proved | all subs proved
| datanode-closed,
datakey-cons,
inodekey-cons,
log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-ro-dentry | proved | all subs proved
| inodes-nodentry,
ubifs-cons,
|
| ubifs-ro-data | proved | all subs proved
| inodes-nodata,
ubifs-cons,
|
| ubifs-ri-cons | proved | all subs proved
| log-cons,
ri-closed,
ubifs-cons,
ubifs-in-fs,
ri-cons,
|
| ubifs-cons-variant4 | proved | all subs proved
| ubifs-log-nodups,
|
| ubifs-cons-variant1 | proved | all subs proved
| ubifs-cons-ino0,
|
| ubifs-cons-ri-closed | proved | all subs proved
| log-cons,
ri-cons,
ubifs-cons,
ubifs-in-fs,
ri-closed,
|
| ubifs-cons-log-cons | proved | all subs proved
| ri-closed,
ri-cons,
ubifs-cons,
ubifs-cons-logadr-in,
log-cons,
|
| ri-cons-variant1-01 | proved | all subs proved
| ri-key-cons,
ri-cons-in,
ri-cons,
|
| ri-cons-empty | proved | all subs proved
| ri-cons-empty-2,
|
| ri-cons-del-orphans | proved | all subs proved
| datakey-cons,
ri-cons,
|
| log-cons-variant1-01 | proved | all subs proved
| log-node-cons,
log-adr-in,
log-cons,
|
| inodes-put | proved | all subs proved
| inodes-in,
inode-set,
|
| inodes-del | proved | all subs proved
| inodes-in,
inode-set,
|
| datalkeys-drop-orphans | proved | all subs proved
| inodes-nodata,
|
| inodes-nodentry | proved | all subs proved
| inode-set,
|
| inodenode-closed | proved | all subs proved
| node-closed,
|
| dentrynode-closed | proved | all subs proved
| node-closed,
|
| datanode-closed | proved | all subs proved
| node-closed,
|
| ubifs-log-nodups | proved | all subs proved
| ubifs-cons,
|
| ubifs-cons-ino0 | proved | all subs proved
| ubifs-cons,
|
| ubifs-cons-logadr-in | proved | all subs proved
| log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-in-fs | proved | all subs proved
| log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ri-cons-in | proved | all subs proved
| ri-cons,
|
| ri-key-cons | proved | all subs proved
| ri-cons,
|
| ri-cons-empty-2 | proved | all subs proved
| ri-cons,
|
| log-adr-in | proved | all subs proved
| log-cons,
|
| log-node-cons | proved | all subs proved
| log-cons,
|
| inodekey-cons | proved | all subs proved
| key-cons,
|
| dentrykey-cons | proved | all subs proved
| key-cons,
|
| inodes-in | proved | all subs proved
| inode-set,
|
| datakey-cons | proved | all subs proved
| key-cons,
|
| inodes-nodata | proved | all subs proved
| inode-set,
|
| ubifs-ro-subset | proved | all subs proved
| log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-log-nodups-add5 | proved | all subs proved
| log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-log-nodups-add4 | proved | all subs proved
| log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-log-nodups-add3 | proved | all subs proved
| log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-log-nodups-add2 | proved | all subs proved
| log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-log-nodups-add1 | proved | all subs proved
| log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-fo-subset | proved | all subs proved
| log-cons,
ri-closed,
ri-cons,
ubifs-cons,
|
| ubifs-cons-ro-inodes | proved | all subs proved
| ubifs-cons,
|
| ubifs-cons-ri-inj | proved | all subs proved
| key-cons,
log-cons,
ri-closed,
ri-cons,
ubifs-cons,
ri-inj,
|
| ubifs-cons-fo-inodes | proved | all subs proved
| ubifs-cons,
|
| ubifs-cons-dom-ri | proved | all subs proved
| ubifs-cons,
|
| ubifs-cons-dom-fi | proved | all subs proved
| ubifs-cons,
|
| truncnode-cons | proved | all subs proved
| node-cons,
|
| ri-inj-write | proved | all subs proved
| ri-inj,
|
| ri-inj-variant1-01 | proved | all subs proved
| ri-inj,
|
| ri-inj-rem | proved | all subs proved
| ri-inj,
|
| ri-inj-empty | proved | all subs proved
| ri-inj,
|
| ri-inj-del | proved | all subs proved
| ri-inj,
|
| ri-cons-truncnode | proved | all subs proved
| key-cons,
ri-cons,
|
| ri-cons-range-ri | proved | all subs proved
| ri-cons,
|
| ri-cons-key | proved | all subs proved
| key-cons,
ri-cons,
|
| ri-cons-inj | proved | all subs proved
| key-cons,
ri-inj,
ri-cons,
|
| ri-cons-gc-one | proved | all subs proved
| ri-cons,
|
| ri-cons-drop | proved | all subs proved
| ri-cons,
|
| ri-cons-copy-new | proved | all subs proved
| ri-cons,
|
| ri-cons-copy | proved | all subs proved
| ri-cons,
|
| ri-closed-variant1-01 | proved | all subs proved
| ri-closed,
|
| ri-closed-gc-one | proved | all subs proved
| node-closed,
ri-closed,
ri-cons,
|
| ri-closed-drop | proved | all subs proved
| node-closed,
ri-closed,
|
| read-lookup-copy | proved | all subs proved
| ri-cons,
|
| nodups-new-nodups | proved | all subs proved
| log-cons,
|
| log-cons-one | proved | all subs proved
| log-cons,
|
| log-cons-emp | proved | all subs proved
| log-cons,
|
| log-cons-drop | proved | all subs proved
| log-cons,
|
| log-cons-copy-old | proved | all subs proved
| log-cons,
|
| log-cons-app | proved | all subs proved
| log-cons,
|
| key-cons-key | proved | all subs proved
| key-cons,
|
| inodenode-cons | proved | all subs proved
| node-cons,
|
| index-update-dom | proved | all subs proved
| key-cons,
ri-cons,
|
| in-ri-update-in-ri | proved | all subs proved
| key-cons,
ri-cons,
|
| file-node-cons-variant1-01 | proved | all subs proved
| file-node-cons,
|
| empty-inodes | proved | all subs proved
| inode-set,
|
| dentrynode-cons | proved | all subs proved
| node-cons,
|
| datanode-cons | proved | all subs proved
| node-cons,
|
| ri-inj | axiom | | |
| file-node-cons | axiom | | |
| inode-set | axiom | | |
| ubifs-cons | axiom | | |
| ri-cons | axiom | | |
| ri-closed | axiom | | |
| log-cons | axiom | | |
| node-cons | axiom | | |
| node-closed | axiom | | |
| key-cons | axiom | | |