[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Lemma dependency for Specification aubifs-base

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:
nodups-newprovedall subs proved write-new-app-nodups,
write-new-app-nodupsprovedall subs proved in-write, new-ext,
write-newprovedall subs proved in-write, new-ext,
new-extprovedall subs proved new-rec, new-base, new-in-fs,
new-in-logprovedall subs proved new-in-fs,
new-in-fsprovedall subs proved new-not-new,
write-new-appprovedall subs proved in-write, new-rec, new-base, new-append,
update-index-appprovedall subs proved update-index-append, index-update-key-base, update-index-one,
read-splitprovedall subs proved read-rec, read-eq-empty, read-base, read-app,
read-eq-oneprovedall subs proved read-eq-empty, read-rec, read-base, read-one,
notin-delsprovedall subs proved at-dels-ro-data, at-dels-ro-nodata, in-dels-ro,
notin-delprovedall subs proved at-del-ro-data, at-del-ro-nodata, in-del-ro,
new-butlastnprovedall subs proved new-append,
keys-in-elim-last-ocprovedall subs proved keys-base, keys-rec, keys-append,
keys-firstnprovedall subs proved keys-rec, keys-base, keys-append,
index-update-at-last-ocprovedall subs proved keys-at-other, index-update-key-rec,
in-dels-inodeprovedall subs proved in-dels-ro,
dels-ignore-dataprovedall subs proved at-dels-ro-data, at-dels-ro-nodata, in-dels-ro,
del-with-empprovedall subs proved datakeys-set-empty, dels-with-data,
del-thisprovedall subs proved at-del-ro-data, at-del-ro-nodata, in-del-ro,
del-put-againprovedall subs proved at-dels-ro-data, at-dels-ro-nodata, in-dels-ro,
del-merge-delsprovedall subs proved at-del-ro-nodata, at-del-ro-data, at-dels-ro-data, at-dels-ro-nodata, in-del-ro, in-dels-ro,
del-del-againprovedall subs proved at-del-ro-data, at-dels-ro-data, at-del-ro-nodata, in-dels-ro, in-del-ro,
del-commute-delsprovedall subs proved at-del-ro-nodata, at-dels-ro-data, at-del-ro-data, at-dels-ro-nodata, in-del-ro, in-dels-ro,
at-write-atprovedall subs proved at-write-other, write-rec,
in-writeprovedall subs proved write-rec, write-base,
update-index-oneprovedall subs proved index-update-key-base, index-update-key-rec,
update-index-appendprovedall subs proved index-update-key-rec, index-update-key-base,
read-appprovedall subs proved read-rec, read-base,
read-oneprovedall subs proved read-base, read-rec,
read-eq-emptyprovedall subs proved read-rec, read-base,
new-not-newprovedall subs proved new-rec,
new-appendprovedall subs proved new-rec, new-base,
keys-appendprovedall subs proved keys-rec, keys-base,
keys-at-otherprovedall subs proved index-update-key-rec, index-update-key-base,
datakeys-set-emptyprovedall subs proved datakeys-set,
in-dels-roprovedall subs proved datakeys-set, dels-with-data,
in-del-roprovedall subs proved datakeys, del-with-data,
at-dels-ro-nodataprovedall subs proved datakeys-set, dels-with-data,
at-del-ro-dataprovedall subs proved datakeys, del-with-data,
at-dels-ro-dataprovedall subs proved datakeys-set, dels-with-data,
at-del-ro-nodataprovedall subs proved datakeys, del-with-data,
at-write-otherprovedall subs proved write-rec, write-base,
write-shiftprovedall subs proved write-rec, write-base,
write-oneprovedall subs proved write-base, write-rec,
write-domprovedall subs proved write-rec, write-base,
write-appprovedall subs proved write-rec, write-base,
update-index-shiftprovedall subs proved index-update-key-rec, index-update-key-base,
update-index-data-notinprovedall subs proved index-update-key-rec, index-update-key-base,
read-write-other-fsprovedall subs proved read-rec, read-base,
read-write-otherprovedall subs proved index-lookup-rec, index-lookup-base,
read-lengthprovedall subs proved read-rec, read-base,
range-inter-empty-inprovedall subs proved range,
range-emptyprovedall subs proved data-in-empty, range,
new-writeprovedall subs proved new-rec, new-base,
new-oneprovedall subs proved new-base, new-rec,
keys-oneprovedall subs proved keys-base, keys-rec,
keys-lengthprovedall subs proved keys-rec, keys-base,
keys-in-elimprovedall subs proved keys-rec, keys-base,
keys-drop-fsprovedall subs proved keys-rec, keys-base,
inode-at-del-datakeysprovedall subs proved datakeys,
index-update-inprovedall subs proved index-update-key-rec, index-update-key-base,
index-update-domprovedall subs proved index-update-key-rec, index-update-key-base,
index-lookup-oneprovedall subs proved index-lookup-base, index-lookup-rec,
index-lookup-lengthprovedall subs proved index-lookup-rec, index-lookup-base,
index-lookup-appprovedall subs proved index-lookup-rec, index-lookup-base,
in-read-in-domprovedall subs proved index-lookup-rec, index-lookup-base,
dentry-at-del-datakeysprovedall subs proved datakeys,
datakeys-set-delprovedall subs proved datakeys, datakeys-set,
datakeys-set-addprovedall subs proved datakeys, datakeys-set,
datakeys-put-inode-01provedall subs proved datakeys,
datakeys-put-inodeprovedall subs proved datakeys-set,
datakeys-put-dentryprovedall subs proved datakeys-set,
datakeys-del-dentryprovedall subs proved datakeys,
datakeys-0provedall subs proved datakeys, datakeys-ge,
data-at-del-datakeysprovedall subs proved datakeys,
read-baseaxiom
read-recaxiom
rangeaxiom
data-in-emptyprovedall subs proved
new-baseaxiom
new-recaxiom
keys-baseaxiom
keys-recaxiom
index-update-key-baseaxiom
index-update-key-recaxiom
index-lookup-baseaxiom
index-lookup-recaxiom
datakeys-geaxiom
write-baseaxiom
write-recaxiom
dels-with-dataaxiom
datakeys-setaxiom
del-with-dataaxiom
datakeysaxiom