[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 persistence-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-commitprovedall subs proved rangeeq-lebs, rangeeq-subarray, rangeeq-concrete-unfold, nat-stuff2, nat-stuff3, idcircle-concrete-write, rangeeq-lebs-5, rangeeq-till-leb5-fwd, rangeeq-subarray-5, id-circle-subarray-concrete-below, prepost-write-superblock, rangeeq-write-right-concrete-below, prepost-write-lebs, prepost-encode-lpt, prepost-write-orphans, commit,
inv-recoverprovedall subs proved prepost-decode-lpt, prepost-read-lebs, prepost-read-orphans, prepost-read-log, prepost-read-superblock, avol-down-size-le, avol-down-mapped-eq, avol-down-size, recover,
prepost-write-orphansprovedall subs proved prepost-encode-orphans, write-orphans,
prepost-read-orphansprovedall subs proved prepost-decode-orphans, read-orphans,
inv-add-log-lebprovedall subs proved prepost-add-log-leb,
inv-formatprovedall subs proved rangeeq-subarray, id-circle-subarray-concrete-below, prepost-write-superblock, rangeeq-write-right-concrete-below, nat-stuff3, nat-stuff2, rangeeq-concrete-unfold, prepost-write-lebs, prepost-encode-lpt, format,
prepost-encode-orphansprovedall subs proved encode-orphans,
prepost-decode-orphansprovedall subs proved ls-del-notin, decode-orphans,
prepost-add-log-lebprovedall subs proved nat-stuff3, nat-stuff2, add-log-leb,
prepost-read-superblockprovedall subs proved read-superblock,
prepost-read-logprovedall subs proved nat-stuff1, read-log,
prepost-read-lebsprovedall subs proved read-lebs,
prepost-decode-lptprovedall subs proved decode-lpt,
prepost-encode-lptprovedall subs proved encode-lpt,
prepost-write-lebsprovedall subs proved write-lebs,
prepost-write-superblockprovedall subs proved write-superblock,
prepost-recover-main-sameprovedall subs proved recover,
inv-get-page-sizeprovedall subs proved get-page-size,
inv-get-leb-sizeprovedall subs proved get-leb-size,
inv-writeprovedall subs proved write,
inv-readprovedall subs proved read,
inv-unmapprovedall subs proved unmap,
inv-remapprovedall subs proved remap,
inv-requires-commitprovedall subs proved requires-commit,
inv-get-volume-sizeprovedall subs proved get-volume-size,
write-superblockaxiom
write-orphansaxiom
write-lebsaxiom
read-superblockaxiom
read-orphansaxiom
read-logaxiom
nat-stuff1provedall subs proved
read-lebsaxiom
encode-orphansaxiom
encode-lptaxiom
decode-orphansaxiom
ls-del-notinprovedall subs proved
decode-lptaxiom
add-log-lebaxiom
get-page-sizeaxiom
get-leb-sizeaxiom
writeaxiom
readaxiom
unmapaxiom
remapaxiom
requires-commitaxiom
get-volume-sizeaxiom
commitaxiom
rangeeq-subarray-5provedall subs proved
rangeeq-till-leb5-fwdprovedall subs proved
rangeeq-lebs-5provedall subs proved
idcircle-concrete-writeprovedall subs proved
rangeeq-lebsprovedall subs proved
recoveraxiom
avol-down-sizeprovedall subs proved
avol-down-mapped-eqprovedall subs proved
avol-down-size-leprovedall subs proved
formataxiom
rangeeq-concrete-unfoldprovedall subs proved
nat-stuff2provedall subs proved
nat-stuff3provedall subs proved
rangeeq-write-right-concrete-belowprovedall subs proved
id-circle-subarray-concrete-belowprovedall subs proved
rangeeq-subarrayprovedall subs proved