[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 ablock-store-inv

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:
to-adrs-eq-appprovedall subs proved adrs-rec, to-adrs-eq-empty, adrs-empty, to-adrs-in, to-adrs-one, to-adrs-append,
prefixn-to-adrsprovedall subs proved to-adrs-eq, to-adrs-append, addresslist-length,
to-adrs-appendprovedall subs proved adrs-rec, to-adrs-eq, adrs-empty,
store-inv-remprovedall subs proved in-store-inv, inv-store,
at-write-sameprovedall subs proved in-in-adr, in-write-same, in, at,
at-write-appprovedall subs proved in-in-adr, in-write-app, in, at,
at-diffprovedall subs proved in-in-adr, in-diff-explicit, in, at,
at-deallocprovedall subs proved in-dealloc, in, at,
in-store-invprovedall subs proved inv-store, inv-flashsize-size, inv-block,
to-adrs-eqprovedall subs proved to-adrs-in, adrs-rec, to-adrs-eq-empty, adrs-empty,
in-write-sameprovedall subs proved notin-notin, in-adr-in, in-in-adr, in,
in-write-appprovedall subs proved to-adrs-in, in,
in-diff-explicitprovedall subs proved in-diff,
in-deallocprovedall subs proved notin-notin, in-adr-in, in-in-adr, in,
to-ards-no-dupsprovedall subs proved to-adrs-in, adrs-rec, adrs-empty,
to-adrs-sublistprovedall subs proved addresslist-length, adrs-rec, adrs-empty,
to-adrs-eq-oneprovedall subs proved to-adrs-eq-empty, adrs-rec, adrs-empty, to-adrs-one,
prefix-remove-refsize0provedall subs proved at-remove-refsize0, in-remove-refsize0, dom-remove-refsize0, inv-block, inv-store, blockstore-prefix,
inv-set-sizesprovedall subs proved inv-flashsize-size, inv-block,
inv-set-refsizeprovedall subs proved inv-flashsize-size, inv-block,
inv-remove-refsize0-diffprovedall subs proved at-remove-refsize0, in-remove-refsize0, inv-flashsize-size, inv-block, inv-store,
inv-remove-refsize0provedall subs proved at-remove-refsize0, in-remove-refsize0, inv-flashsize-size, inv-block, inv-store,
inv-reduce-remprovedall subs proved inv-flashsize-size, inv-block, inv-store,
inv-reduceprovedall subs proved inv-flashsize-size, inv-block, inv-store,
inv-prefixn-laxprovedall subs proved inv-listlen-ls1,
inv-diff-nprovedall subs proved inv-flashsize-size, inv-block, inv-store,
inv-block-emptyprovedall subs proved inv-flashsize-empty, inv-block,
inv-appendprovedall subs proved inv-flashsize-append, inv-block,
inv-allocprovedall subs proved inv-flashsize-size, inv-block, inv-store,
inv-add-nodeprovedall subs proved inv-flashsize-append, inv-block,
at-write-refsizeprovedall subs proved in-in-adr, in-write-refsize, in, at,
at-store-invprovedall subs proved inv-flashsize-size, inv-block, inv-store,
addresslist-in-lnum-simpprovedall subs proved to-adrs-in,
addresslist-inprovedall subs proved to-adrs-in,
to-adrs-oneprovedall subs proved adrs-empty, adrs-rec,
to-adrs-eq-emptyprovedall subs proved adrs-rec, adrs-empty,
addresslist-lengthprovedall subs proved adrs-rec, adrs-empty,
dom-remove-refsize0provedall subs proved in-remove-refsize0,
inv-listlen-ls1provedall subs proved inv-block,
inv-flashsize-emptyprovedall subs proved inv-flashsize,
inv-flashsize-appendprovedall subs proved inv-flashsize,
in-diffprovedall subs proved in,
in-adr-inprovedall subs proved in,
notin-notinprovedall subs proved in,
in-write-refsizeprovedall subs proved in,
inv-flashsize-sizeprovedall subs proved inv-flashsize,
in-in-adrprovedall subs proved in,
to-adrs-inprovedall subs proved adrs-rec, adrs-empty,
to-adrs-dropprovedall subs proved adrs-rec, adrs-empty,
size-oneprovedall subs proved size-base, size-rec,
size-appendprovedall subs proved size-rec, size-base,
remove-refsize0-oneprovedall subs proved at-remove-refsize0, in-remove-refsize0,
remove-refsize0-idemprovedall subs proved at-remove-refsize0, in-remove-refsize0,
remove-refsize0-eq-nonzeroprovedall subs proved at-remove-refsize0, in-remove-refsize0,
remove-refsize0-emptyprovedall subs proved in-remove-refsize0,
prefix-transprovedall subs proved blockstore-prefix,
prefix-set-flagsprovedall subs proved blockstore-prefix,
prefix-rem-leftprovedall subs proved blockstore-prefix,
prefix-rem-allocprovedall subs proved blockstore-prefix,
prefix-remprovedall subs proved blockstore-prefix,
prefix-reflprovedall subs proved inv-block, inv-store, blockstore-prefix,
prefix-notin-fwdprovedall subs proved in, blockstore-prefix,
prefix-just-allocprovedall subs proved blockstore-prefix,
prefix-inprovedall subs proved in, blockstore-prefix,
prefix-fwd-inprovedall subs proved blockstore-prefix,
prefix-empty-rightprovedall subs proved blockstore-prefix,
prefix-empty-leftprovedall subs proved blockstore-prefix,
prefix-domsubsetprovedall subs proved blockstore-prefix,
prefix-del-rightprovedall subs proved blockstore-prefix,
prefix-atprovedall subs proved in, blockstore-prefix, at,
prefix-append-notinprovedall subs proved blockstore-prefix,
prefix-append-inprovedall subs proved blockstore-prefix,
prefix-allocprovedall subs proved blockstore-prefix, inv-block, inv-store,
inv-store-emptyprovedall subs proved inv-store,
inv-nodups-app-leftprovedall subs proved inv-block,
inv-nodupsprovedall subs proved inv-block,
inv-listlen-ls2provedall subs proved inv-block,
inv-flashsize-prependprovedall subs proved inv-flashsize,
inv-flashsize-prefixprovedall subs proved inv-flashsize,
inv-flashsize-appprovedall subs proved inv-flashsize,
inv-eq-list-sizeprovedall subs proved inv-block,
in-write-explicitprovedall subs proved in,
in-emptyprovedall subs proved in,
in-allocprovedall subs proved in,
except-refsizeeq-write-leftprovedall subs proved except-refsize-eq,
except-refsizeeq-transprovedall subs proved except-refsize-eq,
except-refsizeeq-reflprovedall subs proved except-refsize-eq,
except-refsizeeq-commprovedall subs proved except-refsize-eq,
at-explicit-otherprovedall subs proved in, at,
at-explicit-diffprovedall subs proved in, at, inv-block, inv-store,
at-explicitprovedall subs proved in, at, inv-block, inv-store,
at-allocprovedall subs proved in, at,
size-baseaxiom
size-recaxiom
blockstore-prefixaxiom
at-remove-refsize0axiom
inv-flashsizeaxiom
except-refsize-eqaxiom
in-remove-refsize0axiom
inv-storeaxiom
inv-blockaxiom
ataxiom
inaxiom
adrs-emptyaxiom
adrs-recaxiom