[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 ubi-io-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-formatprovedall subs proved write-echdr, inv-read-echdr, format,
inv-read-echdrprovedall subs proved inv-io-read, read-echdr,
inv-read-dataprovedall subs proved inv-io-read, read-data,
inv-read-vidhdrprovedall subs proved inv-io-read, read-vidhdr,
inv-io-readprovedall subs proved io-read,
inv-get-page-sizeprovedall subs proved get-page-size,
inv-get-leb-sizeprovedall subs proved get-leb-size,
inv-recoveryprovedall subs proved recovery,
inv-get-blockcountprovedall subs proved get-blockcount,
inv-isbadprovedall subs proved isbad,
inv-markbadprovedall subs proved markbad,
inv-sync-eraseprovedall subs proved sync-erase,
inv-write-data-wlprovedall subs proved write-data-wl,
inv-write-dataprovedall subs proved write-data,
inv-write-vidhdrprovedall subs proved write-vidhdr,
inv-write-echdrprovedall subs proved write-echdr,
get-page-sizeaxiom
get-leb-sizeaxiom
recoveryaxiom
formataxiom
get-blockcountaxiom
isbadaxiom
markbadaxiom
sync-eraseaxiom
write-data-wlaxiom
write-dataaxiom
read-dataaxiom
write-vidhdraxiom
read-vidhdraxiom
write-echdraxiom
read-echdraxiom
io-readaxiom