[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 btree-asm

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:
inv-commitinvalidinv-commit-rec, commit,
inv-commit-recprovedinv-commit-rec-ind,
inv-commit-rec-indinvalidall subs proved inv-io-save, commit-rec,
inv-io-saveprovedall subs proved io-save,
inv-get-leb-sizeprovedall subs proved get-leb-size,
inv-get-block-free-sizeprovedall subs proved get-block-free-size,
inv-syncprovedall subs proved sync,
inv-requires-commitprovedall subs proved requires-commit,
inv-formatprovedall subs proved format,
inv-read-gndprovedall subs proved read-gnd,
inv-read-gblockprovedall subs proved read-gblock,
inv-get-gc-blockprovedall subs proved get-gc-block,
inv-add-gndsinvalidall subs proved add-gnds,
inv-set-gblock-refsizeprovedall subs proved set-gblock-refsize,
inv-get-gblock-refsizeprovedall subs proved get-gblock-refsize,
inv-allocate-gndprovedall subs proved allocate-gnd,
inv-deallocate-gndprovedall subs proved deallocate-gnd,
inv-recoverprovedall subs proved recover,
inv-is-log-emptyprovedall subs proved is-log-empty,
io-saveaxiom
commit-recaxiom
get-leb-sizeaxiom
get-block-free-sizeaxiom
syncaxiom
requires-commitaxiom
formataxiom
read-gndaxiom
read-gblockaxiom
get-gc-blockaxiom
add-gndsaxiom
set-gblock-refsizeaxiom
get-gblock-refsizeaxiom
allocate-gndaxiom
deallocate-gndaxiom
commitaxiom
recoveraxiom
is-log-emptyaxiom