[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 wbuf-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-enter-readonlyprovedall subs proved enter-readonly,
inv-is-readonlyprovedall subs proved is-readonly,
inv-destroy-bufprovedall subs proved destroy-buf,
inv-get-page-sizeprovedall subs proved get-page-size,
inv-get-leb-sizeprovedall subs proved get-leb-size,
inv-unmapprovedall subs proved unmap,
inv-remapprovedall subs proved remap,
inv-add-log-lebprovedall subs proved move-buf, add-log-leb,
inv-requires-commitprovedall subs proved requires-commit,
inv-commitprovedall subs proved commit,
inv-read-bufprovedall subs proved read-buf,
inv-write-bufprovedall subs proved aligndown-simp, write-buf,
inv-move-bufprovedall subs proved move-buf,
inv-get-volume-sizeprovedall subs proved get-volume-size,
inv-recoverprovedall subs proved recover,
inv-get-bufprovedall subs proved get-buf,
inv-formatprovedall subs proved format,
enter-readonlyaxiom
is-readonlyaxiom
destroy-bufaxiom
get-page-sizeaxiom
get-leb-sizeaxiom
unmapaxiom
remapaxiom
add-log-lebaxiom
requires-commitaxiom
commitaxiom
read-bufaxiom
write-bufaxiom
aligndown-simpprovedall subs proved
move-bufaxiom
get-volume-sizeaxiom
recoveraxiom
get-bufaxiom
formataxiom